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 firstname.lastname@example.org
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.
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
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.
CONTRIBUTION 4: TOOL
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 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 eﬀorts 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 ﬂexible 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 ﬁ- nal user. Moreover, the system also gen- erates a low-level representation of the fuzzy code oﬀering 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
Techniques for the veriﬁcation 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 ﬁeld 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.
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 deﬁned in a modular way. The
control-ﬂow semantics is given by a (ﬁnite) Petri net whose places correspond
to the control locations of the program. The heap semantics is speciﬁed by
transformation rules which describe the eﬀect of executing single commands.
The combination of both yields a labeled transition system (modeled by a
Petri net) which is generally inﬁnite due to the unbounded creation of both con-
trol threads and heap cells. Since in this setting program veriﬁcation is generally
undecidable in this setting we introduce a ﬁrst abstraction, which addresses the
data space of the program. Our list abstraction exploits a variant of summary
nodes  to obtain a ﬁnite 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 inﬁnite [2,3,5]. However, its intractability forces
us to apply a second abstraction step in which we also derive a ﬁnite-state rep-
resentation of the control ﬂow, which altogether yields a ﬁnite 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.
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 modelchecking techniques and tools have been greatly improved by the introduction of bounded modelchecking (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 SATsolvers (such as MiniSat [ES03]). The main goal of the Zot project is to exploit these techniques to offer a userfriendly 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 realtime systems (such as TRIDENT: http://www.elet.polimi.it/res/TRIO/TRIDENT.php). Zot is a small, opensource tool based on robust, opensource 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 logicbased. The tool supports different logic and operational languages through a multilayered 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 densetime 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 ﬁnd 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 efﬁciently 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.
|Email: email@example.com, Phone: +358 2 215 4754, Fax: +358 2 215 4732|