Software Engineering Report

SOFTWARE ENGINEERING 

A report on :

FORMAL DESIGNS IN SOFTWARE ENGINEERING

Introduction

Ever since the first systems appeared, a question has been why systems are not fault free. The simple answer is that even the most rudimentary system is affected by parameters we cannot grasp and stimuli we cannot control. If we

limit the scope of the question to IT systems, the development process itself is full of opportunities to introduce faults and bugs into the code. Formal methods, what they are and how they can reduce the number of faults and bugs, and we present a background describing the development process.

Formal methods in software engineering

In computer science, formal methods are “mathematically rigorous techniques and tools for the specification, design and verification of software and hardware systems” [43]. Mathematically rigorous means that the specification consists of well-formed statements using mathematical logic and that a formal verification consists of rigorous deductions in that logic. The strength of formal methods is that they allow for a complete verification of the entire state space of the system and that the properties that can be proved to hold in the system will hold for all possible inputs. When formal methods cannot be used through the entire development process (due to the complexity of the system, lack of tool or other reasons), they can still successfully be used on parts of the system, for

example for the requirements and high-level design or only on the most safety or security critical components.

The diversity of available formal methods is a result of the different modelling methods and proof approaches needed by different application domains. Also, different development phases of a system might require different tools and techniques. Although many developed formal methods are the result of research efforts in universities, more and more tools and techniques are available outside the academic community. Several of the standards used for system development require formal methods at the highest levels of accreditation. Some examples are the Common.

Background

When a new system is to be implemented, the first step is to write a requirement specification (usually in natural language). The specification should correctly describe the system’s desired behavior and it should be complete

and unambiguous, which can be hard to achieve. The specification is then transformed into code by a programmer, who has to understand the specification correctly and handle any ambiguities. Also, the programmer’s way of coding and solving technical challenges can introduce faults in the code. Then there is the sheer size of the system; nowadays systems are so big that it can be hard to keep track of all the parts to make sure that they correctly follow the specification. Furthermore, there is often a team of programmers working together, which also is a source of faults since they will all have their own interpretations of the specification and of the information shared during the development process. During and after the coding of the system, the system’s functionality is usually tested to make sure that the resulting program satisfies the requirements and that no errors or bugs are present. 

Testing big and complex systems can be very time consuming and, due to the size of the system and the amount of code, an exhaustive testing is not practically feasible.3 Nevertheless when the system is safety and security critical, correct functionality has to be guaranteed, which requires either exhaustive testing or a way of proving that the code correctly implements the specification.

The concept of formal methods introduces tools to mathematically describe

a system (or parts of a system) in a specification and to prove that the resulting program meets the requirements described in the specification. A formal specification is precise and there is no risk for misinterpretations. Also, if there is a proof that the implementation abides by the specification, then one can be sure that the programmers have implemented what is described in the specification. In practice, one cannot completely guarantee that the resulting implementation is fault free, since the formal method used can have defects, or there might be some error in the proof. Nevertheless, increased use of formal methods and tools will result in better and more reliable methods and tools.

To summarize: 

By using formal methods in the system development, errors can be found earlier and some classes of errors can be nearly eliminated. A limitation of formal methods is that they only can be used to prove a system’s correctness with respect to a Specification. Therefore, just because a program has been mathematically proved to abide to the specification, there is no guarantee that the specification in itself is correct and fault free. Nevertheless, properties can be proved on the specification to strengthen the belief that the specification correctly represents the desired functionality.

Classification of formal methods

Almeida et al. [3] present several classifications for formal methods which we use in this chapter. At a general level, formal methods are used in two aspects of software development:

• To enforce the desired behaviour in the specification of the system. A specification is a model of the system that describes its behaviour and formal methods are used for model validation.

• To verify that an implementation has the same behaviour as the specification, or to obtain an implementation that has the same behaviour as the specification. Here one talks about the formal relationship between

implementation and specification. Another general classification of formal methods can be made by considering

how the modelled system is described:

• as a transition system with states, transitions and state transformations,

or

• some program logic with pre- and post-conditions as well as axioms and

inference rules.

A third way to classify formal methods, which we also elaborate on in the remainder of this chapter, is:

1. formal methods used to specify and analyse the specification,

2. formal methods used to specify and prove properties of the specification (formal verification),

3. formal methods used to specify and derive an implementation from the specification, and

4. formal methods used to specify and transform the specification, transformations which either hide details or enrich the specification with extra details.

Specify and analyse

A specification describes the data that the system manipulates and what operations transform the data. The system can be described in two ways. One way is to consider an internal state and to describe the operations that modify this

state. These kinds of specifications of specifications are called model-based or state-based specifications and build a unique model of the system. The second way to describe systems is by focusing on the data that is being manipulated and how the data evolves. These kinds of specifications of specifications are called algebraic specifications and, in this case, there can be many models that provide the required functionality based on the manipulated data. To reduce the number of models, properties of the specification are provided and, commonly, only a few of the models satisfy the required properties. Model-based specifications are described in languages where the internal state is the central point. Such languages are abstract state machines, set and category theories, automata-based modelling and modelling languages for real-time systems. An abstract state machine describes the system in terms of states and state transformations. Some examples of such languages are the B Method together

with the B specification language.

When the set or category theory is used, states are described in terms of mathematical structures such as sets, relations or functions. Transitions are expressed as invariants1, together with pre- and post-conditions. Examples of

set theory formal methods are Z [47] and VDM [34] and examples of category theory methods are Specware and Charity.

Automata are a different class of transition systems, which are particularly adequate to describe concurrent, reactive and communicating systems. Automata can be extended and, as such, used to specify real-time systems. The

most common such automata are timed automata [4], but extensions for modelling of other characteristics of systems such as temperature, inclination or altitude can be found. SCADE  is a complete modelling environment, based on Lustre [15], that can be used to model synchronous concurrent real-time systems. Algebraic specifications concentrate on the specification of data and the input-output behaviour of functions that manipulate data. They are particularly well suited for describing interface specification (i.e., when a large system is divided into several subsystems with well-defined interfaces between them).

Nevertheless, when object operation depends on object state, that is when the result of applying an operation is dependent of the results of previous operations, then algebraic specifications become cumbersome . Sommerville further on claims that a combination of model-based and algebraic specifications defines the overall behaviour of the system.

Furthermore, declarative languages, such as logic-based languages, functional languages and rewriting languages, can be used when writing the specification. Many functional languages are based on the λ-calculus [6] and the

notion of function is a central point of the specification. There also are available

proof assistants like Isabelle [46] and HOL [29] and languages like Haskell based on variants or extensions of the λ-calculus.

Specify and prove

Another aspect of formal methods is to prove properties about the specification (or about the implementation), which is also called formal verification. In order to do formal verification, some logical system has to be used, such as first-order logic or temporal logic. The formal frameworks for verification are divided by Rushby [50, p. 26] in three different levels:

First level 

Demonstrations are carried out by hand with no computer support. Natural languages can be used.

Second level 

Demonstrations are carried out by hand but a rigorous formulation of demonstrations is required.

Third level 

Computer-based tools with support for carrying out demonstrations and proofs.

Different approaches to formal verification exist, such as proof tools, model checking and program annotations. When using proof tools one can choose between logical expressiveness (that gives the possibility to study complex properties) and the simplicity of the logical formalism (that gives the possibility to automatically generate the proof). On one hand, automated theorem provers can be used, which focus on simplicity rather than on expressiveness. The construction of proofs is automatic since they rely on the decidability of the underlying theory. Example of automatic theorem provers are Satisfiability Modulo Theory solvers such as Yices , CVC3 and Z3.

On the other hand, if one needs higher expressiveness, proof assistants can be used where undecidable logic such as higher-order logic is used. Model checking [5] is a technique for verification of finite-state systems broadly used in the industry. The main idea is to express the system with help of temporal logic and then traverse the model entirely and validate the desired properties. If a property is not valid then a counterexample is shown.

The drawback with model checking is state space explosion where the transition graph grows exponentially with the size of the system. There are different techniques available that try to solve the state space explosion problem, for example one can use a higher level of abstraction. Bounded model checking (BMC) is a form of model checking that performs a depth-bounded exploration of the state space, i.e., only states reachable

within a bounded number of steps are explored. Due to the bounded exploration, faults that require a longer path are missed. BMC is mostly used for semiconductor verification although it can also be applied to software.

Program annotations are used to check behavioural properties of programs (source code in particular). An annotation is a logical formula of the specification, placed together with the program whose behaviour is to be verified.

The formula includes the pre and post conditions for that piece of program,for example a method. One specific form of annotations, that is widely spread, is contracts and the runtime verification of contracts. Almost all widespread

programming languages have such a contract layer. For example the JML annotation language2 for Java and the ACSL annotation language for C.

Specify and derive

When a specification with desired properties is available, the next step is to obtain an implementation with a behaviour that matches the specification. There are two solution categories for this step. One is to have a specification that can directly be executed, for example by using logic-based languages like Prolog or functional languages like Scheme and OCalm. Another one is to derive an implementation from the specification. In the first case one already has an implementation that satisfies the desired properties. In the second case one has to prove that the derivation is correct. There are different approaches for how to prove correctness of a derivation. One approach is to focus on the derivation process and prove that it is a correct derivation process. Another approach is to make the derivation process generate a set of proof obligations and prove that they are correct. Therefore either the derivation mechanism or the individual derivation will be subject to formal verification.

A very popular technique, that is used in the industry, is refinement where a program is synthesized step by step from the specification, such that each step increases the degree of precision with respect to the implementation. Steps are implementation choices, such as, which algorithm to use or which data type to choose for a specific variable. Each step is then proved correct. Z, VDM and B use the refinement technique.

Specify and transform

It is often desirable to construct transformations of a specification in order to either abstract details (by approximating them) or to enrich the specification with extra details. The theory of abstract interpretation3 [20] is the main foundation for such transformations. As in engineering, where large problems often are divided into smaller ones, transformations allow for modularity in formal verification. By decomposing

the behaviours of the global model into different views the work is simplified.

In some situations, studying individual aspects can even give equivalent results

to studying the global model. A problem with such transformations is that the abstractions in their general form are easily undecidable. Moreover, transformations are deeply tied to the modelling language used and the properties to be proved. As a consequence, there are a limited number of tools that can be used for such transformations.

Approximations are often done in an ad-hoc fashion and it is hard to make them sound and appropriate.

However, there exists one example of an early ad-hoc model transformation tool set called JaKarTa, which is used for reasoning about JavaCard specifications. JaKarTa provides a rule-based language and transformation specifications based on the effect on the analysed model’s data structures. An example of such transformations is when the focus is on the typing policy of the operational semantics of a virtual machine. By focusing on the typing policy, the actual values are of no interest. The transformation to be performed on the data manipulated by the virtual machine can automatically be passed by JaKarTa on to the operations of the machine and then the soundness of the transformation can be ensured by producing proof obligations in the Coq proof

assistant 

How to choose a formal method

The Formal Methods Europe association has on its website a brief document [25] about what steps to take when beginning with formal methods.

Furthermore, the researchers we have spoken with suggested to find qualified people with a wide background in formal methods, so that they can choose the right formal methods for a specific project.

Which formal method that is most suitable for a specific project is dependent on the kind of system and the kind of properties to be proved. In this chapter we provide classifications over systems and system properties that can

help when choosing a formal method.

Systems classification

According to Klaus Schneider [51], systems can be classified as follows, based on their architecture:

• Asynchronous or synchronous hardware

• Analogue or digital hardware

• Mono- or multi-processor systems

• Imperative/functional/logic-based/object-oriented software

• Multi-threaded or sequential software

• Conventional or real-time operating systems

• Embedded systems or local systems or distributed systems

The author discusses some of the distinguishing characteristics of these systems and what formal methods are most appropriate for them. For example, multithreaded software might require the implementation of complex control tasks and therefore requires a high-level description language. In sequential systems one could use logic-based languages, such as Prolog, and functional languages, such as ML or Haskell. Further, also based on [51], systems can be classified based on the type of interaction:

Transformational systems

Systems that read some input data and produce output. As the output is produced at termination, these systems should always terminate. A compiler is an example of such a system.

Interactive systems

Systems that continuously run and interact with the environment. When the environment gives an action, the system replies with a reaction. The environment has to wait until the system is ready for new actions.

Reactive systems

Similar to interactive systems, only that the environment can freely decide when to start new actions. Therefore the system has to react to a given action before the next action comes. This kind of system falls under the

real-time systems category. Considering this last classification, it is reactive systems that are the most

challenging to implement.

System properties

Many formalisms can be classified by which system properties they can express. A taxonomy of properties is given next, based on:

Safety properties “something bad will never happen”.

Livens properties “something good will eventually happen”.

Fairness properties “some property will infinitely often hold”.

Persistence properties “stabilization of certain properties”. After some point in time, a given property will always hold.

Application domains

Consider that formal methods can be categorized based on the application domain and based on the environmental assumptions. These categories can be used when choosing an appropriate formal method. The

following application domains are considered:

Protocol design and engineering Formal description, and verification, have

been used when designing new protocols. Some protocol specific languages are ESTELLE and SDL, but they have been replaced by more

general languages.

Software design and engineering In this area theoretical foundations and analysis tools are provided by formal methods.

Hardware design and engineering Formal verification tools are widely used which are aimed at detecting design mistakes.

Furthermore, different environments are considered, based on how well understood and predictable they are, with appropriate formal methods suggested for each environment as follows:

Nominal environment which is well-understood and predictable. In such an environment, formal methods focus on correctness and performance issues.

Faulty environment which is mostly understood and predictable, but abnormal events can affect the system. In such environments, the formal methods focus on dependability and performance issues.

Hostile environment which is neither totally understood nor predictable and its behaviour cannot be trusted. In such environments, the formal methods focus on security issues. Both general formal methods and dedicated formal methods have been successfully applied to security issues. For example model checking has been used to find unknown attacks in security protocols. Examples of dedicated formal methods are security-oriented formal notations and software tools for automated analysis of security protocols. Furthermore, in order to ensure security one has to ensure both correctness and dependability. At the same time, formal methods cannot address security issues such as computer hacking, tampering or social engineering.

Where to use formal methods

In this section we give a brief overview of how formal methods have evolved

with time and in what kind of systems they can be used.

To begin with, formal methods were developed for sequential programs focusing on formally proving program correctness. Then concurrent systems were the focus and they were formalized with help of Petri nets1. Here the focus was on message-passing and shared memory. Petri nets were further used for communication systems and distributed and mobile systems. Later formal methods were used in time-critical systems, both for software and for hardware. Both discreet time (reactive systems) and continuous time (hard real-time systems2) can be modelled. Then quality of service and performance evaluation were covered by formal methods. As a result, hard real-time systems, stochastic systems3 and probabilistic systems4 are also covered by formal methods. Formal

methods have also expanded to new application domains such as computer security and bioinformatics. Considering the broad area of use, it is not at all surprising the diversity of methods that exists and the importance of choosing the right method.

Although there are many different formal methods that have been developed (mostly as research projects in academia), there is no broad adoption in the industry with the exception of two areas: mission-critical systems (where mistakes are very expensive and sometimes impossible to correct after the system has been started) and life-critical systems (where there are legal requirements to adhere to specific standards). High-security information systems also require adherence to relevant standards, such as Common Criteria For Information Technology Security Evaluation5. However, Common Criteria only requires formal verification in the highest assurance levels, and there are only a few systems that are evaluated to such levels.

The authors of [28] also discovered that the use of formal methods in industry is not broad, it is mainly used to solve particular issues, and there is consensus neither on which formal methods to use nor for which part of the

development process.

The EU project DEPLOY has on its website several FAQs related to where to use formal methods, for example: What important system concepts can be handled “elegantly” with a selected formal method? 

Limitations of formal methods

In this chapter we discuss the limitations of formal methods. We do not discussthe limitations of any specific formal method, but consider limitations of thearea as a whole.One important question about the use of formal methods is if it results in products with zero defects. The answer is that it results in products with very few defects, close to zero, but that there is still no guarantee that the product will be bug free. Moy and Wallenburg [42] list some reasons for why formally verified products may still contain defects:

• not all parts of the product are formally verified,

• formal verification can only guarantee that the specification has been followed, and therefore only the specified properties can be verified,

• not all properties can be formally verified, for example covert channels can be hard to detect as well as dead code, 

• the formal method and the tools used can have defects, for example the theorem prover.

Proofs can also be wrong, especially if they are done manually. Therefore researchers nowadays recommend the use of automated tools. Another limitation is that there is no way to easily choose a suitable formal method. There are many formal methods available, especially ones developed be research groups in universities, and their maturity varies considerably. Another aspect to consider is the needs of an organization, in terms of people, to start using formal methods. For most formal method tools it should be enough with one specialist in the development team. 



Formal Specifications

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

In each passing decade computer systems have become increasingly more powerful and as a result they have become more impactful to society. Because of this, better techniques are needed to assist in the design and implementation of reliable software. Established engineering disciplines use mathematical analysis as the foundation of creating and validating product design. Formal specifications are one such way to achieve this in software engineering reliability as once predicted. Other methods such as testing are more commonly used to enhance code quality.

Uses

Given such a specification, it is possible to use formal verification techniques to demonstrate that a system design is correct with respect to its specification. This allows incorrect system designs to be revised before any major investments have been made into an actual implementation. Another approach is to use probably correct refinement steps to transform a specification into a design, which is ultimately transformed into an implementation that is correct by construction.

It is important to note that a formal specification is not an implementation, but rather it may be used to develop an implementation. Formal specifications describe what a system should do, not how the system should do it.

A good specification must have some of the following attributes: adequate, internally consistent, unambiguous, complete, satisfied, and minimal.

A good specification will have

Constructability, manageability and resolvability

Usability

Communicability

Powerful and efficient analysis

One of the main reasons there is interest in formal specifications is that they will provide an ability to perform proofs on software implementations.[2] These proofs may be used to validate a specification, verify correctness of design, or to prove that a program satisfies a specification.



Limitations

A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address, since it ultimately concerns the problem constructing abstracted formal representations of an informal concrete problem domain, and such an abstraction step is not amenable to formal proof. However, it is possible to validate a specification by proving “challenge” theorems concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifiers understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved with producing (and implementing) the specification.

Formal methods of software development are not widely used in industry. Most companies do not consider it cost-effective to apply them in their software development processes.[4]This may be for a variety of reasons, some of which are:

Time

High initial start up cost with low measurable returns

Flexibility

A lot of software companies use agile methodologies that focus on flexibility. Doing a formal specification of the whole system up front is often perceived as being the opposite of flexible. However, there is some research into the benefits of using formal specifications with "agile" development[5]

Complexity

They require a high level of mathematical expertise and the analytical skills to understand and apply them effectively[5]

A solution to this would be to develop tools and models that allow for these techniques to be implemented but hide the underlying mathematics[2][5]

Limited scope[3]

They do not capture properties of interest for all stakeholders in the project[3]

They do not do a good job of specifying user interfaces and user interaction[4]

Not cost-effective

This is not entirely true, by limiting their use to only core parts of critical systems they have shown to be cost-effective[4]

Other limitations:[3]

Isolation

Low-level ontologies

Poor guidance

Poor separation of concerns

Poor tool feedback

A Collection of Well-Known Software Failures

Knight Capital's $440 million loss

Incident Date: 8/1/2012    Price Tag: $440 million

Ironic Factor: ****

(The Register) Knight Capital, a firm that specialises in executing trades for retail brokers, took $440m in cash losses Wednesday due to a faulty test of new trading software.

Unfortunately, the trading algorithm the program was using was a bit eccentric as well. On every stock exchange, there is a "bid" and an "ask" price. The bid price is what you'd like to pay the holder of the stock if you want to buy their shares. The ask price is what they'll pay to buy those same shares from you. There's always a spread between the two prices, with the "ask" being a few cents or more above the "bid". If the stock is thinly traded, then the spread between the ask and the bid is higher than what you.d see for, say, IBM.

Knight Capital's software went out and bought at the "market", meaning it paid ask price and then sold at the bid price--instantly. Over and over and over again. One of the stocks the program was trading, electric utility Exelon, had a bid/ask spread of 15 cents. Knight Capital was trading blocks of Exelon common stock at a rate as high as 40 trades per second--and taking a 15 cent per share loss on each round-trip transaction. As one observer put it: "Do that 40 times a second, 2,400 times a minute, and you now have a system that's very efficient at burning money".

As the program continued its ill-fated test run, Knight's fast buys and sells moved prices up and attracted more action from other trading programs. This only increased the amount of losses resulting from their trades to the point where, at the end of the debacle 45 minutes later, Knight Capital had lost $440m and was teetering on the brink of insolvency.



NASA Mars Climate Orbiter

Incident Date: 9/23/1999     Price Tag: $125 million

Ironic Factor: ****

WASHINGTON (AP) -- For nine months, the Mars Climate Orbiter was speeding through space and speaking to NASA in metric. But the engineers on the ground were replying in non-metric English.

It was a mathematical mismatch that was not caught until after the $125-million spacecraft, a key part of NASA's Mars exploration program, was sent crashing too low and too fast into the Martian atmosphere. The craft has not been heard from since.

Noel Henners of Lockheed Martin Astronautics, the prime contractor for the Mars craft, said at a news conference it was up to his company's engineers to assure the metric systems used in one computer program were compatible with the English system used in another program. The simple conversion check was not done, he said.



Therac-25

Incident Date: 6/1985 - 1/1987     Price Tag: three human lives

Ironic Factor: *

(Nancy Leveson, U. of Washington) Between June 1985 and January 1987, a computer-controlled radiation therapy machine, called the Thrace-25, massively overdosed six people. These accidents have been described as the worst in the 35-year history of medical accelerators.

...

(Barbara Wade Rose) ... It turned our that both Yakima accidents, as well as the one at Hamilton, had been caused by another software error -- different from the Malfunction 54. On the Thrace-25, the part of the computer program that is often referred to as the "house-keeper task" continuously checked to see whether the turntable was correctly positioned. A zero on the counter indicated to the technician that the turntable was in the correct position. Any value other than zero meant that it wasn't, and that treatment couldn't begin. The computer would then make the necessary corrections and the counter would reset itself to zero.

But the highest value the counter could register was 255. If the program reached 256 checks, the counter automatically clicked back to zero, the same way that a car odometer turns over to zero after you've driven more than 99,999.99 kilometers. For that split second, the Thrace-25 believed it was safe to proceed when, in fact, it wasn't. If the technician hit the "set" button to begin treatment at that precise moment, the turntable would be in the wrong position and the patient would be struck by a raw beam.