FM 2008

Posters & Research Tools

An exhibition of both research projects and commercial tools will accompany the technical symposium, with the opportunity of holding scheduled presentations of commercial tools. Inquiries may be sent to the Poster and Tools Exhibition Chair, Michael Leuschel (University of Düsseldorf).



CONTRIBUTION 1: TOOL

Title: BART (B Automatic Refinement Tool)

Authors: Thierry Lecomte thierry.lecomte@clearsy.com

Abstract: BART (B Automatic Refinement Tool) is an Atelier B module, enabling the automatic generation of B0 implementation, from a B machine or a sufficiently detailled refinement. BART refinement engine is based on refinement rules database, that define refinement patterns. Rules database can be extended with additional rules during the refinement process.

Demo, Talk


CONTRIBUTION 2: PROJECT

Title: DEPLOY (Industrial Deployment of advanced system engineering methods for high productivity and dependability)

Authors: Jean-Raymond Abrial, Michael Butler, Cliff Jones, Alexander Romanovsky, Kaisa Sere, Elena Troubitsyna

Abstract: The overall aim of the DEPLOY Integrated Project is to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods. The work is driven by the tasks of achieving and evaluating the industrial take-up of the DEPLOY methods and tools, initially in the five sectors which are key to European industry and society.


CONTRIBUTION 3: TOOL

Title: Alloy

Authors: Emina Torlak

Abstract: The Alloy Analyzer is a tool for automatic simulation, checking and debugging of models written in Alloy, a structural modelling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations, and check user-specified properties of a model. For overconstrained models, which rule out interesting behaviors, the Analyzer provides an automatic debugger that highlights the conflicting constraints. Alloy and its analyzer have been used primarily to explore abstract designs, including name servers, network configuration protocols, access control, telephony, scheduling, document structuring, key management, cryptography, instant messaging, railway switching, filesystem synchonization, and semantic web ontologies.

The latest version of the Alloy Analyzer is built on top of Kodkod, an efficient SAT-based analysis engine for first order logic with relations, transitive closure, and partial instances. The Kodkod engine, which includes a finite model finder and a minimal unsatisfiable core extractor, is available freely as a Java API. In addition to powering the Alloy Analyzer, Kodkod is also being used as a backend to several code checkers, a UML analyzer, an automated test case generator, a course scheduler, and a network configuration tool.

Demo


CONTRIBUTION 4: TOOL

Title: Ott

Authors: Peter Sewell, Francesco Zappa Nardelli

Abstract: Ott~[ICFP07] is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle/HOL versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms.

Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, and Isabelle. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), context application functions, and binding auxiliary functions. (At present only a fully concrete representation of binding is supported, without quotienting by alpha equivalence.)

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment. More substantially, Ott has been used for work on LJAM: a Java Module System, by Rok Strnisa~[OOPSLA07], and semantics for OCaml light, by Scott Owens~[ESOP08], both with mechanized soundness proofs.

Poster, Talk, Demo


CONTRIBUTION 5: TOOL(S) and PROJECT

Title: The Mobius Program Verification Environment (PVE)

Authors: Joseph Kiniry, Dan Zimmerman

Abstract The tools that we'd like to demonstrate include:

  • The Mobius Program Verification Environment (PVE)
    A customized version of Eclipse that focuses on reliable systems development.
    See http://mobius.ucd.ie/ and http://mobius.inria.fr/
  • ESC/Java2
    The Extended Static Checker for Java.
  • The JML Tool Suite
    The de facto standard in formal specifications for Java.
    http://www.jmlspecs.org/
  • The FreeBoogie Systema
    An Open Source version of Boogie http://sct.ethz.ch/research/boogie/
    Our website for FreeBoogie is forthcoming.
  • The BONc Tool
    A frontend for reasoning about the BON specification language.
    http://www.bon-method.com/

The Mobius PVE actually integrates ESC/Java2, FreeBoogie, and the JML Tool Suite (among another two dozen subsystems! BONc integration is forthcoming). We focus on the PVE primarily, and the new FreeBoogie and BONc tools secondarily.

2 Talk Slots, Demo


CONTRIBUTION 6: TOOL

Title: The Fuzy Logic Programming Environment FLOPER

Authors: Pedro J. Morcillo, Gines Moreno

Abstract: Declarative programming plays an im- portant role when designing formal methods for software engineering. Fuzzy Logic Programming is an interesting and still growing research area that aggluti- nates the efforts for introducing fuzzy logic into logic programming (LP), in order to incorporate more expressive re- sources on such languages for dealing with uncertainty and approximated rea- soning. The multi-adjoint logic pro- gramming approach represents a re- cent and extremely flexible fuzzy logic paradigm for which, unfortunately, we have not found practical tools imple- mented so far. In this work we describe a prototype system, the FLOPER tool, which is able to directly translate fuzzy logic pro- grams into Prolog code in order to safely execute these residual programs inside any standard Prolog interpreter in a completely transparent way for the fi- nal user. Moreover, the system also gen- erates a low-level representation of the fuzzy code offering debugging (tracing) capabilities and opening the door to the design of more sophisticated program manipulation tasks such as program op- timization, program specialization, pro- gram analysis and so on. In order to support and apply formal methods in industry, we think that the development of such fuzzy logic lan- guages and programing tools might have high relevance, especially when design- ing advanced software applications for medicine, industrial control, and so on.


CONTRIBUTION 7: TOOL

Title: CADP (Construction and Analysis of Distributed Processes)

Authors: Olivier Ponsini

Poster, Demo, Talk

Abstract: CADP stands at the crossroads of "concurrency theory" and "computer-aided verification" and offers a wide range of functionalities for the design of communication protocols and distributed systems (concurrent processes with message-passing communication).

It has been continuously improved since 1986 by the VASY team at INRIA Grenoble - Rhone-Alpes and used in many (over 100) case studies, by industrial and academic users all over the world. CADP is also a well-documented tool with a user forum. In December 2006, a new version of CADP was released, which brought many improvements on existing tools and added 15 new tools.

CADP accepts several input languages, ranging from networks of communicating automata up to higher-level specification languages, such as the ISO standard process algebra LOTOS. For systems specified in this way, CADP supports explicit-state verification according to three paradigms: - Visual checking (graphical inspection of labeled transition systems) - Model checking (satisfaction of a modal mu-calculus formula) - Equivalence checking (minimization and comparison modulo bisimulation and preorder relations)

In addition to verification, CADP also offers: - Rapid prototyping - Random, interactive, or guided simulation - Test case generation - Performance evaluation


CONTRIBUTION 8: TOOL

Title: The rCOS Modeling Tool

Authors: Volker Stolz, Zhiming Liu, Charles Morisset

Abstract: The rCOS Modeling Tool implements the rCOS methodology: it supports use-case driven requirements capture in a multi-view notation. UML class-, sequence, and state diagrams (restricted by the rCOS UML profile) capture the structure and dynamic behaviour of a use case. This separates the different concerns of this stage from each other. Methods of classes are specified with UTP-style pre/post conditions. Static (typing) and dynamic (behaviour in terms of process algebra CSP) consistency of these views are enforced.

After the Requirements Modeling stage, in the Design stage the use cases are refined through "correct by design" refinement steps in rCOS (usually in the sequence diagram- and pre/post specification view) ("Design by drawing"). From this OO-refinement, the component-based architecture is derived. rCOS contracts specify the component interface (again, with behaviour usually described in the dynamic diagrams). Component composition can then be verified again through a process algebra, so this task is also delegated to CSP and FDR2.

From these artefacts, we use the Eclipse Modeling Framework to generate Java skeletons and JML annotations. Parts OF the tool are actually specified IN the tool. Interoperability with other MDD-tools like MagicDraw is possible through the use of UML. A set of sample specifications is available for the "Common Component Modeling Example" (CoCoME http://cocome.org/).

The tool is developed as an Eclipse application on top of TOPCASED. The aim is to offload the various verification and checking tasks to external task like FDR and theorem provers. It is an ongoing project at UNU-IIST headed by Zhiming Liu (3 post-docs, and around 6 master/PhD students spending roughly a year each visiting UNU-IIST as a so-called fellow) and funded by the Macao Science and Technology Fund.

Demo, Talk, Poster


CONTRIBUTION 9: TOOL

Title: State Space Generation for Dynamic Pointer-Manipulating Threads

Authors: Thomas Noll, Stefan Rieger

Abstract: Techniques for the verification of elementary properties of pointer programs are highly desirable. Programming with pointers is error-prone with potential pitfalls such as dereferencing null pointers and the emergence of memory leaks. So far, the field of pointer analysis has primarily focused on sequential programs. But pointer programming becomes even more vulnerable in a concurrent setting where threads can be dynamically created, and where data structures such as linked lists are shared between several threads. We present a tool for state space generation of concurrent programs that operate on singly-linked data structures. It is a (partial) implementation of the concepts in our paper that is going to be presented at FM 2008[4]. In our framework we combine unbounded creation of pointer-manipulating threads and unbounded heap. Our simple concurrent programming language of- fers besides the usual control structures primitives for thread creation, pointer manipulation, cell creation and destruction, and (guarded) atomic regions that allow to implement concurrency control constructs such as test-and-set primi- tives, semaphores, and monitors. The operational semantics of our language is defined in a modular way. The control-flow semantics is given by a (finite) Petri net whose places correspond to the control locations of the program. The heap semantics is specified by transformation rules which describe the effect of executing single commands. The combination of both yields a labeled transition system (modeled by a Petri net) which is generally infinite due to the unbounded creation of both con- trol threads and heap cells. Since in this setting program verification is generally undecidable in this setting we introduce a first abstraction, which addresses the data space of the program. Our list abstraction exploits a variant of summary nodes [1] to obtain a finite representation of the heap and thus eliminates one po- tential source of undecidability. In fact, known results then allow us to conclude that the data abstract model-checking problem is decidable even though the un- derlying transition system is still infinite [2,3,5]. However, its intractability forces us to apply a second abstraction step in which we also derive a finite-state rep- resentation of the control flow, which altogether yields a finite transition system. Both abstractions are sound in the sense that they over-approximate the con- crete program behavior. They can be computed in a fully mechanized manner, and are both implemented in our tool.

References
1. D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of pointers and structures.
In PLDI ’90, pages 296–310. ACM Press, 1990.
2. J. Esparza. On the decidability of model checking for several µ-calculi and Petri nets. In CAAP’94, volume 787 of LNCS, pages 115–129. Springer, 1994.
3. J. L. Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79–104, 1992.
4. T. Noll and S. Rieger. Verifying dynamic pointer-manipulating threads. In 15th International Symposium on Formal Methods (FM ’08). to be published, 2008.
5. H.-C. Yen. A unified approach for deciding the existence of certain Petri net paths. Inf. Comput., 96(1):119–137, 1992.


CONTRIBUTION 10: TOOL

Title: Zot, a flexible bounded model and satisfiability checker

Authors: Matteo Pradella, Carlo A. Furia, Angelo Morzenti, Pierluigi San Pietro

Abstract: In recent years, symbolic model­checking techniques and tools have been greatly improved by the introduction of bounded model­checking (BMC) [CB+01]. BMC is based on the translation of the MC problem into the boolean satisfiability problem (SAT), to exploit the power of current SAT­solvers (such as MiniSat [ES03]). The main goal of the Zot project is to exploit these techniques to offer a user­friendly tool to perform V&V in a TRIO fragment corresponding to a Metric Linear Time Temporal Logic with Past (MPLTL). The tool is available as a simple standalone application, but it can also be easily embedded in a complete environment for the analysis, specification, design, and verification of critical real­time systems (such as TRIDENT: http://www.elet.polimi.it/res/TRIO/TRIDENT.php). Zot is a small, open­source tool based on robust, open­source existing tools (SatLab's SAT2CNF, used in Alloy:  http://alloy.mit.edu, MiniSat, GNU CLisp).  Zot is readily usable for education and experimentation: the source  code is simple and small. Zot is available at http://home.elet.polimi.it/pradella. Zot is currently used for research (see e.g. [PMS07]), and it is presented, together with other toolsets, in the course “Formal Methods” taught by Prof. Dino Mandrioli in the joint programme Politecnico di Milano – University of Illinois at Chicago (UIC). Zot adapts and applies BMC techniques to TRIO, to build a simple and easily modifiable bounded satisfiability checker (BSC). We call this approach bounded satisfiability checking, because it is quite similar to BMC, as it is based on the encoding of a temporal logic into SAT. The main difference resides in the language used to describe the  Model of the system: In BMC this is usually a Büchi automaton, while in BSC everything is described using a temporal logic. This purely descriptive approach, typical of TRIO, benefits from using SAT­ based techniques, being them also logic­based. The tool supports different logic and operational languages through a multi­layered approach: its core uses PLTL, and on top of it MPLTL is defined as a decidable predicative fragment of TRIO. An interesting feature of Zot is its ability to support different encodings of temporal logic as SAT problems. Indeed, the user can choose a particular encoding to carry out verification, while the tool automatically loads the corresponding plugin. This approach encourages experimentation, as plugins are usually quite simple, compact (usually around 500 lines of code), easily modifiable, and extendible. At the moment, a few variants of some of the encodings presented in [BH+06] are supported, together with a bi­ infinite time encoding [PMS07], and the dense­time MTL variant to be presented in [FPR08].


CONTRIBUTION 11: TOOL/ALGORITHM

Title: Automated Static Analysis of SPARK Floating Point Code

Authors: Jan Duracz and Michal Konecny

Abstract: SPARK is a framework for the development and static analysis of programs written in a subset of Ada used primarily for high integrity applications in areas, such as the aerospace, rail and nuclear industries. Many such applications benefit greatly from the use of floating point arithmetic (for example the air traffic control system currently being developed by Praxis HIS Ltd), there is however no standard way of performing round-off error analysis of floating point code in SPARK.

We present a static analysis of floating point arithmetic in the SPARK framework. It is achieved by introducing ghost variables that enable the specification of (abstract) models for floating point arithmetic. Verification conditions (VCs) are then generated and simplified using the standard VC generator and simplifier. The example cases generate VCs that are, at least in principle, tractable with numerical constraint satisfaction techniques. Nevertheless, we demonstrate that existing freely available numerical solvers are insufficient for the purpose of automating the proofs of such VCs.

We give suggestions for improvements of existing numerical techniques and demonstrate their applicability by experiment.

Demo, Poster, Talk


CONTRIBUTION 12: TOOL

Title: Security monitoring tool for .NET mobile devices

Authors: Fabio Massacci Katsiaryna Naliuka

Abstract: Users of mobile devices are increasingly requesting a controlled way to exit from the sandboxing model in order to exploit the full computational power of the device. Porting in-line security monitors to mobile devices helps the user to find a trade-off between security and functionality of the application. Current security monitors provided solutions only for the desktop and either monitor a single instance of an application [Erlingsson 2003; Ligatti et al, 2005] or only to monitor across sessions [Krukow et al, 2005]. We propose to demonstrate a system for in-lined security monitor where simple but expressive logics can be used to specify security policies which can be efficiently monitored.


CONTRIBUTION 13: TOOL

Title: New Developments for ProB

Authors: Michael Leuschel, Jens Bendisposto, Marc Fontaine, Daniel Plagge

Abstract: ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors.

We will present various new developments around the ProB model checker, such as support for Event-B, Z and CSP-M. We will also show the latest symmetry reduction techniques as well as ongoing work to link up ProB with Kodkod.