Gregory M. Kapfhammer

Associate Professor of Computer Science

http://www.cs.allegheny.edu/~gkapfham/

  
View  Edit  Uploads  History  Top  Changes  Search

Ten Commandments of Formal Methods


  • The Second Commandment indicates that a team which uses formal methods should not "overformalize." What does this mean? Give an example of the different "levels" of formal methods and state when these approaches would normally be used.

  • In the Fifth Commandment, the authors state that a team that employs formal methods should not abandon their traditional development techniques. In this Commandment, they note that development occurs later in the lifecycle? How do you reconcile this Commandment in light of agile software development methodologies and technologies?

  • Why is it necessary to test software in a project that uses formal methods? The authors assert that Cyclomatic Complexity can be used to measure the needed testing effort. Do you agree or disagree with this assertion (you might need to do a little digging to learn about cyclomatic complexity, first)?

  • If you had to select a single Commandment as being "the most important", which would you select? Why would you select this commandment?

  • "Overformalizing" is a term that the authors use for the over use of formal methods. Even though formal methods help to increase the confidence in a software system they come at a high cost to use. So using these formal methods in unnecessary situations can lend to high development costs. There are certain situations where conventional methods are the better choice over formal methods such as in domains of informal reasoning. There are three different "levels" of formal methods: formal specification, formal development/verification, and machine-checked proofs. Formal specification helps to give greater insight into system design, dispel ambiguities, maintain abstraction levels and determine the approach and implementation of a problem. This is often helpful for developing complex software architectures and describing their documentation. Formal development/verification involves formally specifying the system, proving certain properties are maintained, and applying a refinement calculus to translate the specifications into concrete representations. This is a full formal development and is rarely used or as the authors state "rarely attempted" due to its rigorous proofs and obvious high costs. Machine-checked proofs help to support consistency and integrity in software systems. This is often used for high-integrity systems, which require high levels of safety and security. The costs may be high for machine-checked proofs, but are often used when failure could cause loss of life, great financial loss, or massive property destruction (ex military programs or financial institutions).

  • In light of agile software development methodologies it seems that this development technique seems to take both from agile software development methodologies and from others like BUFD. This development technique still seems to have the "up front" design type structure except it is broken up into parts that seem to allow for faster and more cost effective designing. Before a design team that uses the traditional development methods begins another team has already been formally analyzing the specifications so that the later design team can get feedback from the earlier one. This eliminates the need of waiting for the formal methods to be developed and integrated and also eliminates the need for a whole team to have to be familiar with the complexities of formal methods.

In your model of software development using formal methods, is it still necessary for the designers to wait until the specificiers have finished making the formal specifications? Doesn't this indicate that these two tasks cannot be interleaved? What parts of a "formal methods development methodology" are like agile software development? Greg

  • No matter how much you would like to believe it, formal methods do not guarantee correctness. They do decrease the chances of bugs in software significantly, but not by 100 percent. Even if the formal methods did happen to pick up all the errors, more errors can be introduced into the system during refinement. The authors assert that cyclomatic complexity (McCabe's Complexity Measure ) can be used to effectively determine the proper amount of testing needed to be done. I agree with this assertion that cyclomatic complexity should be used to determine the amount of testing needed. As comfortable as it would make one feel to completely test a system, but the costs in time, money, and resources to do this testing is high. It is almost unethical to invest in formal methods and that help to ensure confidence in a system and then turn around and test the whole thing. By using cyclomatic complexity one can determine where one should exactly have confidence in a system and where one should still be cautious.

What is cyclomatic complexity? Why do you think that it is a good "measure" of the testing effort that is still needed? Suppose that you worked for a company that clearly stated "we want you to test this software system until you are done." Assuming that you did have the resources for exhaustive testing, wow would you know when you are done testing? Greg

  • It is hard for me to select a single commandment as the best, but I can at least single it down to two: "Thou shalt test, test, and test again" and "Thou shalt reuse". In any software process, both these ideas hold true, but I believe both of these hold truer for formal methods. As this article states, using formal methods although it increases reliability and confidence in a software system it also comes at the cost of time, money, and resources. So we must make sure that we use formal methods wisely meaning that, as stated in the last question, we must test effectively in order to not have put all this work to waste. So thus we must make sure to run our test on only what needs to be tested. This is a special case to formal methods so this is why I believe this to be a good commandment. I have a similar belief about the idea of reuse in this situation. Since we have used formal methods of this software it means that it was (hopefully) well written and would be ideal to use in the future if it can. This way the whole formal method process may not have to be used fully again if we can reuse these previously written segments of code. This is not only good news to the software team (meaning they have to do less work), but also to the higher ups (meaning less in cost).

Brian McAlister


Brenda Gruber

According to the author, overformalizing is when a company "unnecessarily adopts formal methods." The author claims that using formal methods for all parts of the system is unnecessary and costly. To help determine when formal methods should be used, the author suggests three levels of formal methods.

The first level is formal specifications, which are useful because formal languages make specifications more clear and concise. Some examples the author provides are describing the document structure and inconsistencies in the World Wide Web design.

The next level is formal development and verification. This is known as full formal development, that is specifying the system and ensuring that certain properties are maintained and applying calculus to transfer abstract representations into more concrete representations.

The third level are machine checked proofs. These are useful for security and safety critical systems. The hope is that this will help reduce human errors by using mechanical checkers.

The fifth commandment states that a combination of formal methods and alternative methods should be used. They also explain that development occurs later in the lifecycle. This seems to inidicate BUFD and does not correspond to agile software development. Using formal methods does not support agile software development in the traditional way, but as the article suggests, it is possible to use teams.

One team can use traditional techniques and then obtain feedback from another team that uses formal methods. This is similar to the idea of agile programming...design one aspect only with concern for that aspect and the cyclical pattern of designing a little part of the system and having a formal methods "team" analyze are similar.

The author states that testing should still be done regardless if formal methods are used. The formal methods provide an advantage, but cannot guarantee correctness. The author also suggests that testing can find errors created in software during refinement(changing data structures and implementation).

I think that using McCabe's Complexity measure is probably a good idea, but I do not think that the cyclomatic comlexity measure is the only way to determine the needed effort in testing. Cyclomatic complexity "measures the number of linear paths through a software system". It is supposed to determine the exact number of tests needed for a software system. I think that is probably impossible to determine the exact number, especially if we are still using refinement techniques. The number of "necessary test cases" will continue to change. So using McCabe's complexitity may be one of the best techniques to use, it probably shouldn't be the only one.

Just a note: the philosophy behind the usage of cylcomatic complexity is as follows. If a code segment has a high level of cyclomatic complexity, then we must write more test cases for that code segment. We are using cyclomatic complexity as a "proxy" for the actual complexity of a software system. Naturally, we would agree that it is important to invest in a more thorough testing effort for a more complicated program segment. However, it is possible to write very "simple" programs that have high cyclomatic complexity scores and vice versa. We will talk about this more as the semester continues, but I thought that I would ask this question here to introduce you to the topic! Greg

I feel the most important commandment is the fifth commandment concerning the use of traditional methods along with formal methods. I can see the usefulness and the reasons why proponents claim using formal methods is useful, but I do not think it would be wise to elimante alternative methods.

The main reason is the fact that formal methods are hard to understand! Having other ways to express the same thing is probably extremely useful for those with little or no experience with formal methods. One of the iportant facts that we've focused on this semester, particularly with extreme programming, is the idea of communication. In particular communication between designers and users, which sounds similar to the team idea.

So, it seems like there are two approaches: bring all software developers up to a level of mathematical maturity so that they can use formal methods or keep the software development processes that they use at their level. What if undergraduates were trained in the usage of formal methods? Should we not pursue things simply because they are hard? Greg

references:
http://www.sei.cmu.edu/str/descriptions/cyclomatic_body.html

Link to this Page