ESC: Formal spec languages ensure design code quality

But the languages also can be widely used in reactive systems. These are systems that operate repeatedly, in each cycle responding to new inputs and issuing new outputs.

Among the many formal specifications that have been suggested as appropriate for reactive system specification are linear time temporal logic, interval temporal logic, nondeterministic finite automata and branching time temporal logic.

All these specification languages have been shown mathematically to be substantially more economical than any design or programming equivalent. In other words, a deterministic state machine or program that implements a rule, requirement or assertion written in a specification language will generally require resources exponentially larger than the original specification.

This does not mean that programs we build are inefficient. Rather, it means that a specification can be satisfied by many different implementations where each implementation can be efficient, but covers only a subset of the behavior implied by the specification.

Such specification of complex systems and protocols, such as for the PCI bus protocol, have been created in a matter of days. They illustrate the power of specification languages in contrast with formalisms such as state machines or Harel state charts, which are implementation-level formalisms.

The most popular formal specification language is linear temporal logic (LTL). An extension of propositional logic, LTL deals with time and order and was proposed as a way to formally specify mult ithreaded programs. During the last decade-researchers have expanded its theoretical and practical power, using it for example, to specify protocols and hardware.

The syntax of LTL adds eight operators to the AND, OR, XOR and NOT of propositional logic. Four of the operators deal with the future — Always (in the future), Eventually, Until and Next Cycle — and four dual operators address the past — Always in the Past, Sometime in the Past, Since and Previous Cycle.

Inherent to temporal logic is the notion of time, or the definition of a cycle, which is a user-controlled quantity. Two of the applications described later will define their own notion of time.

When considering real-life temporal rules, such as financial or security related temporal rules, there is an evident need for additional operators, most notably counting operators. Though these operators can be mimicked using conventional LTL operators, they tend to make life much easier and result in simpler and easi er to real temporal rules.

Metric temporal logic (MTL), an extension, enhances LTL's capability. With it, you can define upper and lower time constraints, as well as time ranges, for the four LTL future temporal operators. By imposing relative- and real-time constraints on LTL statements, MTL lets you use LTL to verify real-time systems.

Although formal specification are considered to be more intuitive, more economical and easier to use than a conventional programming languages, it is nevertheless expected that human specification errors will eventually occur. For this reason, a temporal logic simulator is clearly desirable.

Formal verification (FV) is the process of proving, mathematically, that a program or hardware module satisfies certain properties, which are typically expressed using a specification language, such as LTL.

The two main general FV meth ods are deductive and algorithmic. Deductive methods typically convert the program and the specification into first order logic and use a prover engine such as Stanford's Step to complete the proof. The primary drawback of deductive methods is that the process is not automatic and requires an expert in the field to complete the process. In addition, proof methods have been developed only for certain patterns of properties such as Always p.

Algorithmic methods are also known as model checkers. Model checkers such as SPIN (AT&T Labs) are completely automatic and work for any LTL specification.

Commercial model checkers are used primarily for the verification of hardware modules written in Verilog-HDL or VHDL. Because of the state explosion problem they are limited to small hardware modules. In addition, model checkers do not support MTL or other LTL extensions and are therefore unable to verify real-time properties.

Because of the limitations of model checking, software designers a re increasingly turning to run-time software verification, a method that combines formal specification methods with conventional run-time testing techniques like hardware and software simulation. This approach to verification takes advantage of automatic verification tools — code generators that produce program code from formal mathematical statements.

Run-time verification (RV) is a hybrid between FV methods and conventional testing. Like FV methods, RV compares a program's behavior against a formal specification, typically in LTL or MTL. However, the actual verification process is not mathematical, albeit automatic; rather, conventional execution based simulation is used. The advantage of conventional testing is its ability to perform automatic verification and regression testing of reactive systems with no need for a costly human test engineer. There are two primary advantages of RV over model checking: RV scales well, enabling automatic verification of real-life, large programs, and it supp orts LTL extensions, including MTL, enabling automatic verification in the field of real-time properties.

There are two main techniques for performing RV. The first is known as the postmortem method. As indicated by its name, it first collects all necessary information while the program is executed, or simulated, for a finite duration.

The postmortem is useful only for verification and does not lend itself to run-time applications, for which the end-time is not known beforehand and LTL evaluation results are required in tandem with program execution. Also, the postmortem method requires large amounts of storage when applied to the verification of lengthy executions.

The second main technique for performing RV is a live method, where LTL specification is converted into a model or source code program that does not grow as time progresses.

The RV technique generates code that is executed in-process with the original program. Frequently, embedded systems are a memory or real-tim e constraint or both in a way that does not permit such an overhead. A particular code generator supports a less intrusive architecture where the in-process code is reduced to a small code snippet that performs open loop communication with a separate verification host. Almost all the code related to temporal verification is then executed on the verification host.

A recent application of formal specification language, in particular LTL and its extensions, is as a programming language. When used as a programming language the formal specification is first converted into conventional C, C++ or Java code using a code generator such as the Temporal Rover, a conversion that is like the compilation process that converts modern programs into machine code.

Unlike all other applications of formal specifications, this application is not concerned with program correctness. Rather, the LTL specification is used as a high-level programming language for programming temporal rules in various security, comme rcial and business applications.

One example of how formal specification improves the way a program handles exceptions would be in a control environment where the formal specification is wrapped around the controller's Java program. Exception code would catch violations of the safety requirement. To do this, it is necessary to describe the safety requirement in LTL and then translate the LTL statements into Java, C or C++ for programs written in those languages, using a code generator such as the Temporal Rover.

When the method detects a failure of the safety requirement, the assertion "throws" (a Java term for "initiates") the exception-handling routine we've designated. Specifically, when the assertion throws the exception, a "catch" function in the main controller routine handles the exception, which in this case changes the light to yellow.

Alternatively, it is possible to accommodate the needs of an observer-based architecture, in which the validation code executes in a se parate process or even on a different machine. In that case, communication with the original program is effected by mechanisms like a remote procedure call or, via the Web, the Hypertext Transfer Protocol (HTTP). The latter is the approach taken by DB-Rover, a tool that validates temporal assertions for databases using HTTP as the communication protocol. If desired, you can add MTL statements to impose relative- and real-time constraints,

Because the code for implementing the temporal assertions executes every cycle whether or not an exception occurs, it can hamper the performance of a program. So it's important to assess the code-generation method for its impact on performance. The most straightforward conversion method and the one used by model checkers is called tableau conversion.

The drawback of this method, which uses LTL-to-automata conversion, is that the generated automaton is both nondeterministic and, worse, grows exponentially with the length of the temporal formula it implement s. What's more, no well-established tableau method exists for handling MTL or LTL extensions. Fortunately, other techniques having less of an impact on performance, including a proprietary one used by Temporal Rover, have been developed for commercial use.

This article is based on excerpts taken from ESC class # 305, Formal specification -based exception handling.