FME on Monday

Detailed program
Monday July 22nd, 2002
See also the unified by-slot program

Sessions take place in auditorium 2 unless otherwise indicated.

All-day activities

FLoC opening

Joint with LICS, RTA
Room: auditorium 1
Chair: Moshe Vardi

08:45-08:55  Introduction and welcome

08:55-09:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof
The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these "little engines of proof" and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modern reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.

Session 1: Testing

Chair: Dines Bjřrner

10:00-10:30  Bruno Legeard, U Franche-Comté, France
Fabien Peureux, U Franche-Comté, France
Mark Utting, U Waikato, New Zealand
Automated boundary testing from Z and B
This article present a method for black-box boundary testing from B and Z formal specifications. The basis of the method is to test every operation of the system at every boundary state using all input boundary values of that operation. The test generation process is highly automated. It starts by calculating boundary goals from Pre/Post predicates derived from the formal model. Then each boundary goal is instantiated to a reachable boundary state, by searching for a sequence of operations that reaches the boundary goal from the initial state. This process makes intensive use of a set-oriented constraint technology, both for boundary computation and to traverse the state space. The method was designed on the basis of industrial applications in the domain of critical software (Smart card and transportation). Application results show the effectiveness and the scalability of the method. In this paper, we give an overview of the method and focus on the calculation of the boundary goals and states.

Session 2: Testing

Chair: Bernhard Aichernig

11:00-11:30  Gil Ratsaby, IBM Haifa, Israel
Baruch Sterin, IBM Haifa, Israel
Shmuel Ur, IBM Haifa, Israel
Improvements in coverability analysis
In simulation-based verification users are faced with the challenge of maximizing test coverage while minimizing testing costs. Sophisticated techniques are used to generate clever test cases and to determine the quality attained by the tests. The latter activity, which is essential for locating areas of the design that need to have more tests, is called test coverage analysis. We have previously introduced the notion of coverability, which refers to the degree to which a model can be covered when subjected to testing. We showed how a coverability analyzer enables naive users to take advantage of the power of symbolic model checking with a 'one-button' interface for coverability analysis. In this work, we present several heuristics, based on static program analysis and on simulation of counter examples, for improving the efficiency of coverability analysis by symbolic model checking. We explain each heuristic independently and suggest a way to combine them. We present an experiment that shows improvements based on using random simulation in the analysis of coverability.

11:30-12:00  Juan C. Burguillo-Rial, U Vigo, Spain
Manuel J. Fernández-Iglesias, U Vigo, Spain
Francisco J. Gonzáles-Castańo, U Vigo, Spain
Martín Llamas-Nistal, U Vigo, Spain
Heuristic-driven test case selection from formal specifications. A case study
We propose an approach to testing that combines formal methods with practical criteria, close to the testing engineer's experience. It can be seen as a framework to evaluate and select test suites using formal methods, assisted by informal heuristics. This proposal is illustrated with a practical case study: the testing of a protocol for mobile auctions in a distributed, wireless environment.

12:00-12:30  Igor B. Bourdonov, ISP/RAS Moscow, Russia
Alexander S. Kossatchev, ISP/RAS Moscow, Russia
Victor V. Kuliamin, ISP/RAS Moscow, Russia
Alexander K. Petrenko, ISP/RAS Moscow, Russia
UniTesK test suite architecture
The article presents the main components of the test suite architecture underlying UniTesK test development technology, an automated specification based test development technology for use in industrial testing of general-purpose software. The architecture presented contains such elements as automatically generated oracles, components to monitor formally defined test coverage criteria, and test scenario specifications for test sequence generation with the help of an automata based testing mechanism. This work stems from the ISP RAS results of academic research and 7-years experience in industrial application of formal testing techniques.

Session 3: Semantics and logic (In memory of John Dawes)

Chair: John Fitzgerald

14:00-14:30  David von Oheimb, Techn. U of Munich, Germany
Tobias Nipkow, Techn. U of Munich, Germany
Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited
We define NanoJava, a kernel of Java tailored to the investigation of Hoare logics. We then introduce a Hoare logic for this language featuring an elegant new approach for expressing auxiliary variables: by universal quantification on the outer logical level. Furthermore, we give simple means of handling side-effecting expressions and dynamic binding within method calls. The logic is proved sound and (relatively) complete using Isabelle/HOL.

14:30-15:00  Juan Bicarregui, Rutherford Appleton Laboratory, UK
Do not read this
We discuss the interpretation of read and write frames in model-oriented specification taking the B's generalised substitutions as the vehicle for the presentation. In particular, we focus on the interpretation of read frames, the semantics of which have not been considered by previous authors. We gives several examples of the relevance of read frames and show that a substitution admits a read respecting implementation if and only if a certain bisimulation condition is satisfied. We use this to motivate a richer semantic model for substitutions which interprets read and write constraints directly in the denotation of a substitution. This semantics yields some non-interference results between substitutions which cannot be given at this level without the use of read and write frames.

15:00-15:30  Niels Jřrgensen, U Roskilde, Denmark
Safeness of make-based incremental recompilation
The make program is widely used in large software projects to reduce compilation time. make skips source files that would have compiled to the same result as in the previous build. (Or so it is hoped.) The crucial issue of safeness of omitting a brute-force build is addressed by defining a semantic model for make. Safeness is shown to hold if a set of criteria are satisfied, including soundness, fairness, and completeness of makefile rules. Conditions are established under which a makefile can safely be modified by deleting, adding, or rewriting rules.

Session 4: Model checking support for analysis

Chair: José Oliveira

16:00-16:30  Thomas Arts, Ericsson, Sweden
Clara Benac Earle, U Kent-Canterbury, UK
John Derrick, U Kent-Canterbury, UK
Verifying Erlang code: a resource locker case-study
In this paper we describe an industrial case-study on the development of formally verified code for Ericsson's AXD 301 switch. For the formal verification of Erlang software we have developed a tool to apply model checking to communicating Erlang processes. We make effective use of Erlang's design principles for large software systems to obtain relatively small models of specific Erlang programs. By assuming a correct implementation of the software components and embedding their semantics into our model, we can concentrate on the specific functionality of the components. We constructed a tool to automatically translate the Erlang code to a process algebra with data. Existing tools were used to generate the full state space and to formally verify properties stated in the modal µ-calculus. As long as the specific functionality of the component has a finite state vector, we can generate a finite state space, even if the state space of the real Erlang system might be infinite. In this paper we illustrate this by presenting a case-study based on a piece of software in Ericsson's AXD 301 switch, which implements a distributed resource locker algorithm. Some of the key properties we proved are mutual exclusion and non-starvation for the program.

16:30-17:00  Alexandre Mota, Federal U of Pernambuco, Brazil
Paulo Borba, Federal U of Pernambuco, Brazil
Augusto Sampaio, Federal U of Pernambuco, Brazil
Mechanical abstraction of CSPZ processes
We propose a mechanised strategy to turn an infinite CSPZ process (formed of CSP and Z constructs) into one suitable for model checking. This strategy integrates two theories which allow us to consider the infiniteness of CSPZ as two separate problems: data independence for handling the behavioural aspect and abstract interpretation for handling the data structure aspect. A distinguishing feature of our approach to abstract interpretation is the generation of the abstract domains based on a symbolic execution of the process.

17:00-17:30  Sharon Barner, IBM Haifa, Israel
Shoham Ben-David, IBM Haifa, Israel
Anna Gringauze, IBM Haifa, Israel
Baruch Sterin, IBM Haifa, Israel
Yaron Wolfsthal, IBM Haifa, Israel
An algorithmic approach to design exploration
In recent years, the technique of symbolic model checking has proven itself to be extremely useful in the verification of hardware. However, after almost a decade, the use of model checking techniques is still considered complicated, and is mostly practiced by experts. In this paper we address the question of how model checking techniques can be made more accessible to the hardware designer community. We introduce the concept of exploration through model checking, and demonstrate how, when differently tuned, the known techniques can be used to easily obtain interesting traces out of the model, rather than used for the discovery of hard-to-find bugs. We present a set of algorithms, which support the exploration flavor of model checking.

17:30-18:00  Michael Huber, Siemens Transportation Systems, Switzerland
Steve King, U York, UK
Towards an integrated model checker for railway signalling data
Geographic Data for Solid State Interlocking (SSI) systems detail site-specific behaviour of the railway interlocking. This report demonstrates how five vital safety properties of such data can be verified automatically using model checking. A prototype of a model checker for Geographic Data has been implemented by replacing the parser and compiler of NuSMV. The resulting tool, gdlSMV, directly reads Geographic Data and builds a corresponding representation on which model checking is performed using NuSMV's symbolic model checking algorithms. Because of the large number of elements in a typical track layout controlled by an SSI system, a number of optimisations had to be implemented in order to be able to verify the corresponding data sets. We outline how most of the model checking can be hidden from the user, providing a simple interface that directly refers to the data being verified.

19:00-21:00  City Hall reception

Joint with LICS, RTA
Room: City Hall