Formal Verification and Conformance Testing for Reactive Systems
Document Actions
Medicine. Airlines. Telecommunication. Nuclear plants. Automobile...
Computers play a substantial and ever-increasing role in sensitive fields. With
activity a glitch away from potentially nasty backwash, security is of
essence. These security requirements
have led to the development of specific programming languages and related
verification tools.
Vlad Rusu (1) focuses his work on systems in which a set of events
triggers a set of actions in return. These programs that continuously react to
their environment are referred to as reactive systems. They rely on what is
called formal methods, ie: mathematically-based techniques for the
specification, development and verification of software and hardware.
At the current state of the art, computer-assisted proofs of correctness remain time-consuming and thus freakingly expensive. Conducting a verification case study on the ATM-SSCOP protocol (2) with the help of PVS proof assistant (3), Rusu reckons he “was able to finish the survey in three months. A relatively reasonable time span for quite a hefty case. But a duration that remains well below industry standard”, he comments. Lengthy tedious work makes price tag high and keep the scope of formal methods therefore limited to fields where the benefits of having such proofs makes them worth spending the extra buck.
Rusu’s research contributions have concentrated on two main directions so far. First: “attempting to make theorem-proving based verification applicable to larger examples, by combining it with other techniques such as abstraction and compositional reasoning.” Secondly: “combining formal verification with conformance testing techniques, in order to establish the correctness of black-box (4) implementations of reactive systems with respect to their specifications and/or to other higher-level properties.”
“I believe I have illustrated the fact that verification and testing (whether conformance testing or other) are complementary on an operation level but also in a methodology of formal validation at system level, in particular reactive systems, Rusu claims. There is a future for the integration of a methodology, the integration –and combining- of verification and testing, but also other formal techniques such as controller synthesis and fault diagnosis.” All of these are ongoing research at Vertecs (5).
Rusu opines the stumbling block in the development of larger-scale industrial applications is the fact that “tools haven’t reached full maturity yet. There is often a lack of specifications and properties.” The raw material, so to speak. But Rusu sees “more than a promising start in some industries. In circuits for instance, model checking is routinely used for testing the equivalence of different views of a circuit. In software also: a tool like Slam allows the fully automatic checking of some C program standard properties for a subset of the language.” The Slam analysis engine forms the core of a bug-spotting tool called Static Driver Verifier (SDV) that systematically analyzes the source code of Microsoft Windows device drivers using model checking techniques.
Formal verification consists in “proving a program or a software, against properties that are themselves formally defined.” There are various ways of tackling the problem. The first approaches “consisted in considering correctness as a theorem and trying to prove it… manually”. But paper-and-pencil proving is “quickly limited by the sheer size of the nowadays programs. Hence, the idea of using computers for helping, systematizing, mechanizing the correction.”
Depending on the manner computers get involved in these proof and correction attempts, scientists distinguish algorithmic techniques (like model checking or abstract interpretation) and deductive techniques (whereby the user interacts with a proof assistant). These approaches can themselves been combined in numerous fashions.
An alternative to verification (in order to improve our confidence in program correction) is testing. The goal is here “less ambitious than program correctness. The purpose is not to guarantee total flawlessness, at least against a given property (like in verification), but to find mistakes… as many of them as possible.”
“In verification, Rusu remarks, the question that keeps coming back is: how to sensitize the industry to our methods?” One way of achieving this is by “weaving links with the (semi-formal) methods, the notations that people are already familiar with, so that they could start using formal methods without even noticing it. John Rushby (6) coined the expression: invisible formal methods. These are as unobtrusive as, for instance, a compiler or a word processor. And just as intuitive.”
Is it bound to happen in the real world? “I don’t know. (…) A key target application for conformance testing is security. Cryptographic protocols in particular. This is virgin turf that we have to occupy. The stakes are so high in computer security that may be, formal models will yield benefits.”
-----
Footnotes
(1)
A member of the VERTECS project team, Vlad Rusu
presented various aspects of his research on formal verification and
conformance testing for reactive systems during his HDR defence, last December.
The HDR (Habilitation à Diriger des Recherches) is an accreditation to
supervise research. See video here.
(2) ATM (Asynchronous Transfer Mode) is a network protocol which encodes data into small (53 bytes) fixed-sized cells instead of variable sized packets (like IP or Ethernet would do). Service Specific Connection Oriented Protocol (SSCOP) is a data link layer protocol in the B-ISDN suite that guarantees the delivery of ATM signalling packets. For more about these research by Vlad Rusu, see: Verifying an ATM Protocol Using a Combination of Formal Techniques (2004) and Verifying an ATM Protocol Using a Combination of Formal Techniques in The Computer Journal.2006; 49: 710-730.
(3) PVS: Specification and Verification System. PVS is a specification language integrated with support tools and a theorem prover. An open source research prototype, PVS is intended to capture the state-of-the-art in mechanized formal methods.
(4) White box and black box testing are terms used to describe the point of view a developer takes when designing a test. Black box refers to an external view of the test object, i.e. executable code. White box refers to an internal view, i.e. source code.
(5) VERTECS stands for: VERification models and techniques applied to the TEsting and Control of reactive Systems. The aim of this Irisa project team is to improve the reliability of reactive systems by providing software engineers with methods and tools for automating the test generation and controller synthesis from formal specifications.
(6) Program director for formal methods in the Computer Science Laboratory at Stanford Research Institute (SRI), California, John Rushby leads the group that has developed the PVS theorem prover.
Previous stories :
Analysis, Modelling and Simulation for Human Movements
Better Interoperability for Healthcare Information Systems
Peerple at Paris Linux Expo 07
Kerlabs in the Wake of Kerrighed
INRIA in Expert Group on Java Resource Management