Talk:Formal methods

Model Checkers

One of the most important model checkers is Java Pathfinder. It should be added. — Preceding unsigned comment added by 190.84.60.204 (talk) 04:43, 7 June 2012 (UTC)

Proponents and critics are the same peoples.So article is incorrect.

How can a discussion of software development processes not include the Unified Process? A complete discussion of XP but not one mention of UP. Biased in my opinion.

RUP is not a formal method. RUP has no theorem prover. RUP has no Z-like notation. Just writing prose requirements is not "formal". —optikos 16:27, 5 November 2006 (UTC)

Do you mean the so-called Unified Developing Method authored by a popular Gang-of-four? That is not a formal method, roughly semi-formal. This article is not about such methods nor a comparison of formal vs. semi-formal vs. informal methods. I agree with Optikos. E2806:106E:B:50B6:44D1:9C42:AC2A:EE80 (talk)

Old Example

I'm not sure this example is really appropriate; it's one specific method out of many. At a minimum, the tone is too informal. I'm going to move it here for now and perhaps work on incorporating it later. Jim Huggins 21:32, 26 Apr 2005 (UTC)

Thowa 10:42, 17 Apr 2005 (UTC): None of the formal methods can be shortly explained within a Wiki-discussion. But let's do a short example, a more interested reader might find as a useful starting point to understand how powerful formal methods in practise are.

Let's create a finite state machine (FSM) having two states "Eat" and "Sleep". This FSM shall communicate with two external objects: a digital input (di) and a timer (ti). The digital input can generate two signals: “true” and “false”. The timer generates one signal “over”. The timer accepts also a command “start” (which does a reset and starts the timer). We create an input and output dictionary which can be used by the FSM:

Input dictionary

{di_true, di_false, ti_over}

Output dictionary

{ti_start}

What does our example FSM do? It starts in state “Eat” and goes to state “Sleep” in case the di was set to “true”. Entering the state “Sleep” the FSM starts the timer. To go back to state “Eat” the timer must be “over” (ti_over) and the di must be changed to “false” (di_false). Please print the FSM transition diagram on a piece of paper to avoid any misunderstanding. To create the executable specification we need to create state transition tables for each state of our FSM:

State Name	Condition(s)	Actions(s)
Eat (current state)	Entry action	n/a
Sleep (next state)	di_true	n/a

and

State Name	Condition(s)	Actions(s)
Sleep (current state)	Entry action	ti_start
Eat (next state)	di_false AND ti_over	n/a

An automatic process can generate a set of equations which fully express the above specification. This set could look like this (note that this is already a kind of machine code, so it looks criptical, but I enter it here to show the “magic” behind the executable specification):

S1 N2 V4 S2 E1 N1 V3&2

where S represents the current state, N the next state, E entry action and V condition (& means AND). For instance the first line means “in state 1 (Eat) go to state 2 (Sleep) if the boolean condition 4 (di_true) is true”.

Some words about the used boolean algebra here. In the presented concept it is the positive logic algebra and not the boolean algebra (i.e. NOT is forbidden). The reason is simple: in the software world we have very seldom signals which can be negated. Lets take for instance a sensor which delivers temperature: temp_low, temp_good and temp_high. What would be NOT temp_high? So in the above concept we only look if a signal exists or not. Some signals cannot exists in parallel, e.g. We cannot have at the same time di_true and di_false.

The above equation plus the description of the I/O dictionaries can be now read by a standard executor (which might be a part of the OS) and executed.

Verification

It is true that an automated theorem-prover requires human assistance simply because the logic is (normally) too expressive, but what is the rationale for claiming that model-checking approaches "quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model"? What is a "sufficiently abstract model"? What does it mean to get "bogged down"? Finally, why does it matter? // Mats Kindahl 06:28, 19 June 2006 (UTC)

This was presumably written by someone trying to provide a "balanced point of view". But I agree that the statement isn't particularly clear or useful. It'd probably be better to substitute a (referenced) sentence that describes the weaknesses of model-checking. --Allan McInnes (talk) 15:29, 19 June 2006 (UTC)

References

Moved from article --Allan McInnes (talk) 18:44, 23 December 2006 (UTC)

I am missing a number of references:

1. David Gries, the science of programming 2. C. Hoare, lots of articles about proving programs 3. E. Dijkstra, another writer who has written a lot about proofing programs, especially about semaphores and such. —The preceding unsigned comment was added by 86.87.79.130 (talk • contribs).

Please add machine checkable proofs

What seems to be missing in this article is the middle ground between hand-written mathematical proofs and automatic theorem proving. The interactive theorem provers like Isabelle, Coq, etc. allow writing proofs that are machine checkable. -- Hritcu 11:17, 22 January 2007 (UTC)

Please feel free to add any material you think the article is missing. --Allan McInnes (talk) 04:11, 23 January 2007 (UTC)

Type Systems

Formal methods are not only about correctness. Type systems are also considered (lightweight) formal methods, and their goal is to prevent runtime errors by static analysis. There are many other static analysis methods. -- Hritcu 11:54, 22 January 2007 (UTC)

I'm not sure that I see the distinction you are trying to make here. A well-typed program is "correct" in the sense that it does not have any type inconsistencies. As a consequence of that correctness, it will not produce runtime type errors. If your concern is that the article doesn't mention type systems and other static analysis methods, then I agree that it would be good to have some discussion of such things. --Allan McInnes (talk) 04:26, 23 January 2007 (UTC)

Hritcu, I don't understand your assertion, I think that you are confusing a (religious) discussion that many programmers have about preferring "typed" or "not typed" (really single type) languages.

I agree with Allan McInnes. Let me add more about the subject.

The type system often plays an important role in structuring programs. And are the basis on how to represent information in the specification. Think about a RDBS if it is ill structured, the compiler wont report errors during static analysis, if the known anomalies like lost of information will occur during the use of the system, an analogous problem arises within very bad structured OO systems, when the design is based in anthropomorphic metaphors instead of a well grounded theoretical foundation. — Preceding unsigned comment added by 2806:106E:B:50B6:44D1:9C42:AC2A:EE80 (talk) 01:31, 25 February 2022 (UTC)

Change of tone - there is no fight

Personally I don't like the tone of the article, which presents formal methods like some very controversial topic people are arguing about. Sure there are proponents, and critics, but the article focuses almost entirely on this debate. Like the article mentions, by now people have very much understood that formal methods are no silver bullet. They have advantages and disadvantages and they are all quite well understood. Why not have the focus on advantages/disadvantages rather than on pointless flamewars. -- Hritcu 11:17, 22 January 2007 (UTC)

I wholeheartedly agree. --Allan McInnes (talk) 04:28, 23 January 2007 (UTC)

Also, totally agree. I've found this on other IT articles as well, writing the article as if it has to present the two most extreme views of the subject (e.g. OOP solves all software problems! vs. OOP is rubbish!) the emphasis IMO shouldn't be on presenting the debate between the most vociferous advocates and detractors but in objectively describing the pros and cons. --MadScientistX11 (talk) 16:29, 14 February 2014 (UTC)

Hritcu, now I partially agree with you, that fictitious competition among formal methods is what motivated me to write a comment here. I am more radical than all you because I don't even support a comparison focused in advantages/disadvantages. I think is just sufficient to say what each method is more useful for, more adequate. They complement each other. There is no "best" winner.

In a medical checkup your blood samples will just give a picture of your health, your weigh, blood pressure, temperature and oxygenation are other parameters, x-ray and ultrasound images other, and so on, which is better or sufficient?

There is no one "mighty method", proof assistants are not used for the same kind of analysis than model checkers. The semantic model depends on what you want to do, prove your program (algorithm) correct or derive it? implement an interpreter/compiler? you see there is no point in that stupid competition approach in which all we agree to remove. But a comparison based on advantages/disadvantages in my opinion don´t seem the best way to expose it, because they were developed for different goals. An advantages/disadvantages comparison only works for things made for the same purpose. I said, (an emoticon for a deep breath here). — Preceding unsigned comment added by 2806:106E:B:50B6:44D1:9C42:AC2A:EE80 (talk) 02:22, 25 February 2022 (UTC)

Criticisms Section Contains Facts, Not Criticisms

• "internal criticisms" ? What does this mean?
• proving correctness requires a long time (and time means money) - duh, it is a fact not a criticism, like all the other statements in this section. Sure, it would be nice to have references for these claims, but they seem pretty much common sense, and they are not critical, to justify having them in a criticisms section. On the other hand the article is full of "critics say" statements which would very well suit this section, since they make the article look like a slashdot discussion not an encyclopaedia entry. -- Hritcu 11:31, 22 January 2007 (UTC)

Few thoughts about your post:
1) I think it is nice to have the common sense ("fact") written for people who don't know the subject.
2) I disagree with you that it is a common sense. In fact, many Formal Methods' proponents preach for it being widely applied in any field, not only high risk systems. So I think Criticism is the right place for it.
3) I don't really follow your reasoning... You think it is a obvious "fact", but at the same time you say it require references.
4) In some cases, placing "critics say" is a nice way to show what opponents say about it, while showing NPOV. And I don't understand why you think an Encyclopedia can't show when something has disagreements (like widely using formal methods against not using it).SSPecter ^Talk|E-Mail ◆ _{17:50, 5 November 2007 (UTC)}.

This is criticism: "Of course, it is widely believed that there is no silver bullet for software development," And it is quite debatable. I mean, the software crisis is exactly that: lack of formality! —Preceding unsigned comment added by 128.62.163.208 (talk) 20:27, 25 July 2008 (UTC)

Who watches the watchmen?

"Verifying the verifier" is an instance of a deeper philosophical problem named "Who watches the watchmen?". So I added an interdisciplinary link to Quis custodiet ipsos custodes? in the text of the article. --Antonielly (talk) 18:15, 14 November 2008 (UTC)

Test-Driven Development

Should Test-driven_development be considered a newer formal method?

Crowne (talk) 22:03, 9 March 2009 (UTC)

Tests are a formal specification of behaviour -one's machines can read- but they tend to be unsuited for formal proofs of correctness, at least when procedural languages are used to write the tests. SteveLoughran (talk) 13:21, 10 March 2009 (UTC)

"the sub-discipline of programming language semantics"

This encroachment is contradicted by the ACM classification system where "formal methods" is only a level-4 leaf. It certainly does not include programming language semantics in the ACM classification. This article, as well as the associated Wikipedia categories have been written/populated by someone with an obvious vested interest in enlarging the meaning of "formal methods". It reminds me of those mathematician that try to include computational complexity theory in computability theory despite the fact that the common view in computer science (c.f. theory of computation, which mostly follows the ACM classification) is that the two are distinct. On this wiki a number of prominent computer scientists have been categorized as "formal methods people", from Alan Turing to Don Knuth, none of which identified themselves as such, nor did they work in this fields as usually defined; they would certainly be theoretical computer science people as that notion is used nowadays, but that's far wider category. Pcap ping 15:09, 23 August 2009 (UTC)

I think I've addressed the issue. I've used a book written by a "formal methods person" as source. Pcap ping 18:51, 23 August 2009 (UTC)

Level taxonomy

This article currently says that formal methods can be used at different levels, namely Levels 0 to 2. Does this leveling imply increasing quality of formal methods with respect to correctness? And if so, what is the difference in quality between Level 1 (formal development and formal verification) and Level 2 (theorem prover)? --Abdull (talk) 09:17, 11 September 2010 (UTC)

I can't find any source for any such formalized taxonomy of formal methods. Additionally, the information in the list of levels contains a lot of unsourced opinion. I think the entire Taxonomy section could be renamed to "Approaches" and rewritten to better explain how these approaches are actually used in practice. Cryolophosaur (talk) 04:15, 18 March 2024 (UTC)

Proposed merge with Formal methods and large scale systems

I don't really see why a separate article about FM in large systems is needed; also, Formal methods and large scale systems has some pretty generic examples of FMs in practical use. QVVERTYVS (hm?) 16:08, 14 February 2014 (UTC)

Makes sense to me. I support the merge. --MadScientistX11 (talk) 16:22, 14 February 2014 (UTC)

It looks like there is no Formal methods and large scale systems article anymore, it looks red to me, so I'll remove the merge notice since it makes no sense to merge without something that doesn't exist anymore, right? Sofia Koutsouveli (talk) 23:57, 17 March 2014 (UTC)

Indeed, and thanks for that, but I'm going to contact the admin who removed the other article. It had some content that deserved merging here. QVVERTYVS (hm?) 09:48, 18 March 2014 (UTC)

NO, please don't do that!

Formal methods are used for other kind of systems too, not just large scale systems.

PLEASE DON'T MERGE, they are different things! — Preceding unsigned comment added by 2806:106E:B:50B6:44D1:9C42:AC2A:EE80 (talk) 02:48, 25 February 2022 (UTC)

Proposed merge with Formal Methods and Data Intensive Systems

Recreation of Formal methods in large scale systems, discussed earlier. QVVERTYVS (hm?) 10:16, 19 March 2014 (UTC)

The article Formal methods in large scale systems seems to be deleted again which is IMO as it should be. I don't see the point in bringing back an article because you think some parts of it were worth merging into an existing article. If you think that then just rewrite the Formal methods article and add the new stuff. But I'm against bringing back that other article, it had a tag on it that indicated it was more a personal recollection and it clearly just overlaps this article. MadScientistX11 (talk) 12:45, 19 March 2014 (UTC)

The thing is that I'm not really familiar with the topic and the author of the other article seems to be so. Now, his material is all gone, including all of the examples of real-world applications of formal methods and a host of references to relevant work. QVVERTYVS (hm?) 14:12, 19 March 2014 (UTC)

Is there a way to look at that old article without recreating it? I am familiar with the topic, not an expert as some of the people who contributed are but I've done some formal methods work in the real world and read a fair bit of the literature. I could take a look at the old article and see if there is anything that stands out as really needing to be brought back. My guess is that there isn't much that was lost, the merge process is supposed to take care of that, before the article was deleted anything that other editors thought worth saving would have been put into this article. But I'm willing to take a look but I don't know how to see that deleted article. BTW, another thing that could be done is to create a user file with the old article and leave a comment in the Talk page with a link to that file. I would be more comfortable with that kind of a solution because a user page is not part of the encyclopedia. MadScientistX11 (talk) 14:28, 19 March 2014 (UTC)

I think you have to be an admin to see deleted pages. The other option is to request undeletion while promising to userfy the page to your own space. QVVERTYVS (hm?) 15:03, 19 March 2014 (UTC)

The merge proposal that was just set up doesn't work properly, it just links back to the same article as the article that is proposed for merger. Essentially, it's a proposal to merge the article with itself -- which is rather interesting from a formal methods perspective, a probably correct meaning preserving transformation ;-) but not something that I think should be kept. If someone can give me a link to the old article, I will create a new talk section and save that old article in a user page under my namespace (of course if someone else wants to do that so much the better) so that the content isn't lost and can be merged back in as appropriate but I continue to think it's not a good idea to recreate the deleted article. To do that we are essentially starting the merge discussion all over again. I'm not convinced it's even worth the trouble so I'm not going to spend time contacting an admin and doing that part myself. MadScientistX11 (talk) 17:44, 19 March 2014 (UTC)

That's because I already redirected the other article here after merging the main stuff. You need to look at the latest version as a full article. QVVERTYVS (hm?) 21:32, 19 March 2014 (UTC)

Btw. the other article wasn't deleted at all. QVVERTYVS (hm?) 21:32, 19 March 2014 (UTC)

Now that I've actually read the article I really don't understand why you are putting any effort into this. The page you linked to is poorly written and comes off as some bachelor's student in computer science who has gone through one formal methods class. It adds nothing and IMO parts of it are simply wrong. Talking about how even small problems in large scale systems somehow means that formal methods are appropriate is not accurate. I know people who are strong proponents of formal methods and even they would say as much. Formal methods aren't justified or very useful in making some transaction or Internet system a few percentage points more efficient. Where they are valuable is in things like mission critical software, weapons or security where one mistake can mean you lose lives or someone cracks your code. Or in the design of hardware where a mistake means you have to remake the chip. And the stuff that wasn't wrong was just boilerplate that is already in this article and written in a more professional way than that one was. MadScientistX11 (talk) 23:55, 19 March 2014 (UTC)

It's the references more than the text (which is largely a sales pitch for the author's own publications): the other article cites examples of where formal methods were used in industrial practice, something that was entirely missing from this article. I think I merged the most important bits now. QVVERTYVS (hm?) 13:23, 20 March 2014 (UTC)

AGAIN NO, please don't do that!

Formal methods are used for other kind of systems too, not just data intensive systems.

AGAIN, PLEASE DON'T MERGE, they are different things! — Preceding unsigned comment added by 2806:106E:B:50B6:44D1:9C42:AC2A:EE80 (talk) 02:53, 25 February 2022 (UTC)

Level Taxonomy reference missing or level construct not appropriate

I did not find such general consensus information in lately papers Applying Formal Methods to Networking: Theory, Techniques, and Applications by Junaid Qadir and Osman Hasan has some sort of taxonomy, though they differ in Soundness,Automation,Counter Examples and Generic "Most of the static analysis tools compromise the soundness to improve completeness of the analysis" -> soundness as criteria, a table would be great though I am not sure if i can just insert the table of the paper or what the general scientific consens is [System Theory view also missing using Lyapunov functions] anyone found another paper with a good overview over all/most usable solvers + taxonomy? — Preceding unsigned comment added by 134.61.102.191 (talk) 23:04, 29 October 2016 (UTC)

CC BY SA 3.0

GFDL Ramadan.halitii (talk) 14:20, 11 March 2017 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Formal methods. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf to http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 04:26, 4 October 2017 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified 3 external links on Formal methods. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20060301022259/http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html to http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html
• Added archive https://web.archive.org/web/20060309041943/http://home0.inet.tele.dk/pgl/fmtrends98.pdf to http://home0.inet.tele.dk/pgl/fmtrends98.pdf
• Added archive https://web.archive.org/web/20130404202524/http://academic.research.microsoft.com/Keyword/14916 to http://academic.research.microsoft.com/Keyword/14916

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 13:50, 22 December 2017 (UTC)

Don't propagate the myth that "formal methods are not cost-effective"

The article asserts things like:

... formal methods lite. This may be the most cost-effective option in many cases.

... fully formal machine-checked proofs. Despite improving tools and declining costs, this can be very expensive and is only practically worthwhile if the cost of mistakes is very high ...

That is false. The real problem is

... Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

yes even today there is a lack of people who can do that work. Commercial software is developed is released prematurely to "gain the market".

The maintenance cost of ill written programs may accumulate years of work. While the time invested doing a good analysis, specification and design is much more that the time needed to carelessly write a program quickly. With formal methods the maintenance cost is much more lower because, ideally, it is mainly required due to changes in the requirements, contrary to fixing mistakes (bugs) produced when the programs are carelessly written on the rush.

Today many people prefer to write disposable programs instead because they perceive that it is not worth to invest the time needed to use formal methods to make sure that they do correctly what is required to do. After all with all the accumulated experience they have, they make less errors each time. There is no apparent gain in learning all the sophisticated mathematics required to understand and use formal methods.

That is more a cultural issue, I think that the article should not mention nothing about cost-effectiveness, because that is not really true, is more a social issue, due to an education systems along the world that makes students to perceive that mathematics are too complicated.

Hi! 100% agreed, and happy to help with discussing and improving the article in this regard. By the way, your comments are unsigned and you aren't logged in -- would you be willing to create an account and sign your comments by adding four tildes at the end? Best regards, Caleb Stanford (talk) 18:51, 28 February 2022 (UTC)

re List of companies that use formal methods in industry

Hi @Liebfrautits: I reverted your recent edit as I don't think including a self-published Git link is appropriate, but many of the entries in the table are sourced -- if you're interested, perhaps you could include some of that information here (with the original source), I think that would be very welcome. Caleb Stanford (talk) 03:07, 15 September 2023 (UTC)