FME 2001 - Symposium Programme
[ FME 2001 ]

[ Wednesday, 14th March: sessions 1 (Invited talk), 2, 3, 4a, 4b |
Thursday, 15th March: sessions 5 (Invited talk), 6, 7, 8a, 8b |
Friday, 16th March: sessions 9 (Invited talk), 10, 11, 12a, 12b ]

  Wednesday, 14th March

9:00 - 9:30

Opening

Session 1: Invited talk
Chair: Wolfgang Reisig ( Humboldt-Universität zu Berlin, Germany )

9.30 - 10.30

Lightweight Formal Methods
Daniel Jackson ( Laboratory for Computer Science, Massachusetts Institute of Technology, USA )

Abstract: Formal methods have offered great benefits, but often at a heavy price. For everyday software development, in which the pressures of the market don't allow full-scale formal methods to be applied, a more lightweight approach is called for. I'll outline an approach that is designed to provide immediate benefit at relatively low cost. Its elements are a small and succinct modelling language, and a fully automatic analysis scheme that can perform simulations and find errors. I'll describe some recent case studies using this approach, involving naming schemes, architectural styles, and protocols for networks with changing topologies. I'll make some controversial claims about this approach and its relationship to UML and traditional formal specification approaches, and I'll barbeque some sacred cows, such as the belief that executability compromises abstraction.

10.30 - 11.00

Coffee Break

Session 2: Proof and model-checking
Chair: Lars-Henrik Eriksson ( Industrilogik L4i AB, Sweden )

11.00 - 11.30

Reformulation: a Way to Combine Dynamic Properties and B Refinement
F. Bellegarde , C. Darlot , J. Julliand , O. Kouchnarenko (Laboratoire d'Informatique de l'Université de Franche-Comté 16, route de Gray , 25030 Besançon Cedex )

Abstract: We are interested in verifying dynamic properties of reactive systems. The reactive systems are specified by B event systems in a refinement development. The refinement allows us to combine proof and model-checking verification techniques in a novel way. Most of the PLTL dynamic properties are preserved by refinement, but in our approach, the user can also express how a property evolves during the refinement. The preservation of the abstract property, expressed by a PLTL formula F1, is used as an assumption for proving a PLTL formula F2 which expresses an enriched property in the refined system. Formula F1 is verified by model-checking on the abstract system. So, to verify the enriched formula F2, it is enough to prove some propositions depending on the respective patterns followed by F1 and F2. In this paper, we show how to obtain these sufficient propositions from the refinement relation and the semantics of the PLTL formulae. The main advantage is that the user does not need to express a variant or a loop invariant to obtain automatic proofs of dynamic properties, at least for finite state event systems. Another advantage is that the model-checking is done on an abstraction with few states. (Keywords: Verification of PLTL properties, Combination of proof and model-checking, Refinement development.)

11.30 - 12.00

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries
Steffen Helke , Thomas Santen (Technische Universität at Berlin Institut für Kommunikations und Softwaretechnik FR 5-6, Franklinstrasse 28/29, D-10587 Berlin )

Abstract: We report on an analysis of the inheritance relationships in the Eiffel Base Libraries, a library of container data structures. If inhertance is behaviorally conforming, then polymorphism can be used safely, and the inheritance hierarchy can be considered part of the interface of the library to its clients. We describe a theory of object-oriented specification in higher-order logic that we used to specify part of the Eiffel Base Libraries. With the theorem prover Isabelle/HOL, we mechanically prove conformance relationships between those specifications. This work allows us to draw conclusions about the design of the Eiffel Base Libraries, and about the feasability of using an interactive theorem prover to apply a strictly formal theory to the specification of a commercial product.

12.00 - 12.30

Proofs of Correctness of Cache-Coherence Protocols
Joseph Stoy ¹ , Xiaowei Shen ² , Arvind ² ( ¹ Oxford University Computing Laboratory ; ² MIT Laboratory for Computer Science, 545 Technology Square,Cambridge Ma 02139 USA )

Abstract: We describe two proofs of correctness for Cachet, an adaptive cache-coherence protocol. Each proof demonstrates soundness (conformance to an abstract cache memory model CRF) and liveness. One proof is manual, based on a term-rewriting system [5, 15] definition; the other is machine-assisted, based on a TLA [17] formulation and using PVS [10]. A two-stage presentation of the protocol simplifies the treatment of soundness, in the design and in the proofs, by separating all liveness concerns. The TLA formulation demands greater precision about what aspects of the system's behavior are observable, bringing complication to some parts which were trivial in the manual proof. The systematic examination of the protocol, necessary for the construction of the mechanical proof, revealed a previously unnoticed imperfection of the protocol design.

12.30 - 14.00

Lunch

Session 3: Model checking
Chair: Augusto Sampaio ( Universidade Federal de Pernambuco, Brasil )

14.00 - 14.30

Model-Checking Over Multi-Valued Logics
Marsha Chechik , Steve Easterbrook , Victor Petrovykh (Department of Computer Science, University of Toronto Toronto ON M5S 3G4, Canada )

Abstract: Classical logic cannot be used to effectively reason about systems with uncertainty (lack of essential information) or inconsistency (contradictory information often occurring when information is gathered from multiple sources). In this paper we propose the use of quasi-boolean multi-valued logics for reasoning about such systems. We also give semantics to a multi-valued extension of CTL, describe an implementation of a symbolic multi-valued CTL model-checker called Xchek, and analyze its correctness and running time.

14.30 - 15.00

How to Make FDR Spin LTL Model Checking of CSP by Refinement
Michael Leuschel ¹ , Thierry Massart ² , Andrew Currie ¹ ( ¹ Department of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK ; ² Computer Science Department University of Brussels, ULB - CP 212 Bld du Triomphe B-1050 Brussels, Belgium )

Abstract: We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking (of CSP processes) using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between "classical" model checking and refinement checking.

15.00 - 15.30

Avoiding State Explosion for Distributed Systems with Timestamps
Fabrice Derepas ¹ , Paul Gastin ² , David Plainfossé ¹ ( ¹ Nortel Networks 1, Place des frères Montgolfier, BP 50 MS BA/53 78928 Yvelines Cedex 09, France. ; ² LIAFA, UMR 7089 case 7014 Université Paris 7 2, place Jussieu F-75251 Paris Cedex 05, France )

Abstract: This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking many distributed systems. Timestamps are often used to keep track of the relative order of events. They are usually implemented with very large counters and therefore they generate state explosion. The aim of this paper is to present a very efficient reduction of the state space generated by a model checker when using timestamps. The basic idea is to map the timestamps values to the smallest possible range. This is done dynamically and on the fly by adding to the model checker a call to a reduction function after each newly generated state. Our reduction works for model checkers using explicit state enumeration and does not require any change in the model. Our method has been applied to an industrial example and the reduction obtained was spectacular. (Keywords: Formal verification, State explosion problem, Timestamp, Distributed systems.)

15.30 - 16.00

Coffee Break

Session 4a: Security
Chair: Friederike Nickl ( Swisslife, Germany )

16.00 - 16.30

Secrecy-preserving Refinement
Jan Jürjens (Computing Laboratory, University of Oxford, GB )

Abstract: A useful paradigm of system development is that of stepwise refinement. In contrast to other system properties, many security properties proposed in the literature are not preserved under refinement (refinement paradox). We present work towards a framework for stepwise development of secure systems by showing a notion of secrecy (that follows a standard approach) to be preserved by standard refinement operators in the specification framework FOCUS (extended with cryptographic primitives). We also give a rely/guarantee version of the secrecy property and show preservation by refinement. We use the secrecy property to uncover a previously unpublished flaw in a proposed variant of TLS, propose a correction and prove it secure. We give an abstract specification of a secure channel satisfying secrecy and refine it to a more concrete specification that by the preservation result thus also satisfies secrecy.

16.30 - 17.00

Information Flow Control and Applications - Bridging A Gap -
Heiko Mantel (German Research Center for Artificial Intelligence (DFKI), Stuhlsatzenhausweg 3, D-66123 Saarbruecken, Germany )

Abstract: The development of formal security models is a difficult, time consuming, and expensive task. This development burden can be considerably reduced by using generic security models. In a security model, confidentiality as well as integrity requirements can be expressed by restrictions on the information flow. Generic models for controling information flow in distributed systems have been thoroughly investigated. Nevertheless, the known approaches cannot cope with common features of secure distributed systems like channel control, information filters, or explicit downgrading. This limitation caused a major gap which has prevented the migration of a large body of research into practice. To bridge this gap is the main goal of this article.

Session 4b: Agent architectures
Chair: Dominique Mery ( Université Henri Poincaré, France )

16.00 - 16.30

A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures
V.S. Alagar , Z. Xi (Department of Computer Science, Concordia University Montreal, Quebec H3G 1M8, Canada )

Abstract: The main issue in the development of agent-based architectures for E-Commerce applications is to produce specifications that describe precisely the functional and temporal properties of agents and their roles. An agent should be able to dynamically change its behavior according to the context of its collaboration. Interactions among agents must remain secure and consistent with E-Commerce business rules. Formal modeling, and analysis of agent-based architectures promote understanding and reasoning on these issues. This paper presents a theory of agents, and a formal description of an E-Commerce architecture. The visual and formal descriptions are complementary, leading to validation and verification prior to committing to an implementation.

16.30 - 17.00

A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware
Nalini Venkatasubramanian ¹ , Carolyn Talcott ² , Gul Agha ³ ( ¹ Dept. of Information and Computer Science, Univ. of California Irvine, Irvine, CA 92697-3425 ; ² Department of Computer Science, Stanford University, Stanford, CA 94305 ; ³ Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801 )

Abstract: Systems that provide QoS-enabled services such as multimedia are subject to constant evolution - customizable middleware is required to effectively manage this change. Middleware services for resource management such as scheduling, protocols providing security and reliability, load balancing and stream synchronization, execute concurrently with each other and with application activities and can therefore potentially interfere with each other. To ensure cost-effective QoS in distributed systems, safe composability of resource management services is essential. In this paper we present a meta-architectural framework for customizable QoS-based middleware based on the actor model of concurrent active objects. Using TLAM, a semantic model for specifying and reasoning about components of open distributed systems, we show how a QoS brokerage service can be used to coordinate multimedia resource management services in a safe, flexible and efficient manner. In particular, we show that a system in which the multimedia actor behaviors satisfy the specified requirements, provides the required multimedia service. The behavior specification leaves open the possibility of a variety of algorithms for resource management as well as adding additional resource management activities by providing constraints to ensure their non-interference. (Keywords: meta-object models, distributed systems, theoretical foundations, object-oriented applications, multimedia.)

  Thursday, 15th March

Session 5: Invited talk
Chair: Pamela Zave ( AT&T Labs Research, USA )

9.30 - 10.30

A Programming Model for Wide-Area Computing
Jayadev Misra (Univ. of Texas at Austin, Austin, USA)

Abstract: During the last decade there have been great strides in broadband communication, and the world-wide-web provides a giant repository of information. This combination promises development of a new generation of distributed applications, ranging from mundane office tasks --e.g., planning a meeting by reading the calendars of the participants-- to real-time distributed control and coordination of hundreds of machines --e.g., as would be required in a recovery effort from an earthquake.

The distributed applications we envisage have the structure that they collect data from a number of sources, compute for a while and then distribute the results to certain destinations. This simple paradigm hides a multitude of issues. When should an application start executing: when invoked by a human, by another application, periodically say, at midnight, or triggered by an event, say, upon detection of the failure of a communication link? How does an application ensure that the data it accesses during a computation is not altered by another concurrently executing application? How do communicating parties agree on the structure of the data being communicated? And, how are conflicts in a concurrent computation arbitrated? In short, the basic issues of concurrent computing such as, exclusive access to resources, deadlock and starvation, and maintaining consistent copies of data, have to be revisited in the wide-area context.

There seems to be an obvious methodology for designing distributed applications: represent each device (computer, robot, a site in the world-wide-web) by an object and have the objects communicate by messages or by calling each others' methods. This representation maps conveniently to the underlying hardware, and it induces a natural partition on the problem that is amenable to step-wise refinement. We start with this model as our basis, simplify and enhance it so that it is possible to address the concurrent programming issues. In this talk, I discuss the programming model and some of our experience in building distributed applications.

10.30 - 11.00

Coffee Break

Session 6: Object-oriented formal modelling
Chair: Nico Plat ( West Consulting, The Netherlands )

11.00 - 11.30

A Formal Model of Object-Oriented Design and GoF Design Patterns
Andres Flores ¹ , Richard Moore ² , Luis Reynoso ¹ ( ¹ Department of Informatics and Statistics - University of Comahue, Buenos Aires 1400, 8300 Neuquen, Argentina ; ² UNU/IIST, P. O. Box 3058, Macau )

Abstract: Particularly in object-oriented design methods, design patterns are becoming increasingly popular as a way of identifying and abstracting the key aspects of commonly occurring design structures. The abstractness of the patterns means that they can be applied in many different domains, which makes them a valuable basis for reusable object-oriented design and hence for helping designers achieve more effective results. However, the standard literature on patterns invariably describes them informally, generally using natural language together with some sort of graphical notation, which makes it very difficult to give any meaningful certification that the patterns have been applied consistently and correctly in a design. In this paper, we describe a formal model of object-oriented design and design patterns which can be used to demonstrate that a particular design conforms to a given pattern, and we illustrate using an example how this can be done.

11.30 - 12.00

Validation of UML models thanks to Z and Lustre
Lydie Du Bousquet , Sophie Dupuy (Laboratoire LSR-IMAG, BP 72, 38402 Saint Martin d'Hères cedex, France )

Abstract: Graphical notations such as UML are very popular thanks to their simplicity and their intuitive aspect. Nevertheless their lack of precise semantics limitates the possibility of the specification validation. So we propose here to translate some of the UML models into Z and Lustre formal specifications in order to use a theorem prover and a test generator to validate the models. This approach is presented on the "cash-point" service case study proposed during the world Formal Method congress 1999 tool contest.

12.00 - 12.30

Components, Contracts, and Connectors for the Unified Modelling Language UML
Claus Pahl (School of Computer Applications, Dublin City University, Dublin 9, Ireland )

Abstract: The lack of a component concept for the UML is widely acknowledged. Contracts between components can be the starting point for introducing components and component interconnections. Contracts between service providers and service users are formulated based on abstractions of action and operation behaviour using the pre- and postcondition technique. A valid contract allows to establish an interconnection - a connector - between the provider and the user. The contract concept support the re-use of components by providing means to establish and modify component interconnections. A flexible contract concept shall be based on a refinement relation for operations and classes, derived from operation abstractions. Abstract behaviour, expressed by pre- and postconditions, and refinement are the key elements in the definition of formal and flexible component and component interconnection approach.

12.30 - 14.00

Lunch

Session 7: Real time systems
Chair: Jim Woodcock ( Oxford University, UK )

14.00 - 14.30

An Integrated Approach to Specification and Validation of Real-Time Systems
Adnan Sherif , Augusto Sampaio , Sérgio Cavalcante (Federal University of Pernambuco Center of Informatics P.O. BOX 7851 Cidade Universitaria 50740-540 Recife - PE Brazil )

Abstract: This work presents an integrated approach which covers from the formal specification to the analysis and use of tools to prove properties about real-time systems. The proposed language to specify the system behaviour is Timed-CSP-Z, a combination of Timed CSP and Z. We propose a rule-based strategy for converting a Timed-CSP-Z specification to TER Nets, a high level Petri Net based formalism with time. The conversion enables us to use the CABERNET tool to analyse desired properties. As a practical case study we discuss the application of this approach to the specification and analysis of an On-board Computer of a Brazilian microsatellite.

14.30 - 15.00

Real-Time Logic Revisited
Stephen Paynter (Matra BAe Dynamics (UK) Ltd, Filton, Bristol, UK )

Abstract: This paper redefines RTL within classical many-sorted logic with arithmetic. In doing so, RTL is generalised in a number of ways. In particular, functionality is handled through the use of timed variables. Various models of time for RTL are discussed, and it is argued that, providing events satisfy a finite occurrence property, time in RTL can be continuous. A number of useful RTL theorems are stated, and it is shown that RTL can naturally express all the usual temporal requirements that are placed on real-time systems. RTL is compared with other timed logics.

15.00 - 15.30

Improvements in BDD-based Reachability Analysis of Timed Automata
Dirk Beyer (Software Systems Engineering Research Group, Technical University Cottbus, D-03013 Cottbus, Postfach 10 13 44, Germany )

Abstract: To develop efficient algorithms for the reachability analysis of timed automata, a promising approach is to use binary decision diagrams (BDDs) as data structure for the representation. The size of a BDD is very sensitive to the ordering of the variables. This paper shows that the communication structure of the timed automata can be used to find good variable orderings to have compact BDDs, which leads to an efficient reachability analysis. We develop a discrete semantics for closed timed automata to get a finite state space required by the BDD-based representation and we prove the equivalence to the continuous semantics regarding the set of reachable locations. An upper bound for the size of the BDD representing the transition relation and an estimation for the set of reachable configurations based on the communication structure is given within this paper. Experiments on different case studies, using a tool implementing these concepts, justify our assumption: Polynomial reachability analysis seems to be possible for some classes of models. (Keywords. Timed automata, Discretization, BDDs, Formal verification, Real-time systems.)

15.30 - 16.00

Coffee Break

Session 8a: Concurrency and parallelism
Chair: Jayadev Misra ( University of Texas at Austin, USA )

16.00 - 16.30

Serialising Parallel Processes in a Hardware/Software Partitioning Context
Leila M. Silva ¹ , Augusto Sampaio ² , Geraint Jones ³ ( ¹ UFS, Aracajú, Brazil ; ² DI-UFPE Recife, Brazil ; ³ Oxford University Computing Lab., Oxford, UK )

Abstract: In this paper we present a strategy to serialise parallel processes in Occam, in the context of a hardware/software partitioning approach. The strategy takes as input two parallel processes to serialise and applies algebraic rules to perform the serialisation. These rules are derived from the semantics of Occam, which guarantees that the serialisation strategy preserves the semantics of the original parallel processes. In particular, the strategy ensures that deadlock is not introduced during the serialisation procedure.

16.30 - 17.00

Verifying Implementation Relations
Jon Burton ¹ , Maciej Koutny ¹ , Giuseppe Pappalardo ² ( ¹ Department of Computing Science, University of Newcastle, Newcastle upon Tyne NE1 7RU, U.K. ; ² Dipartimento di Matematica e Informatica, Viale A.Doria 6, Università degli Studi di Catania, I-95125 Catania, Italy )

Abstract: Implementation relations are a means to relate the behaviour of implementation and specification systems built of communicating processes in the event that respective implementation and specification processes have differing interfaces. In this paper we first present a graph-theoretic statement of such relations and then derive algorithms for their automatic verification. (Keywords: Behaviour abstraction, communicating sequential processes, compositionality, verification.)

Session 8b: Logic and Foundations
Chair: Eerke Boiten ( University of Kent, UK )

16.00 - 16.30

An Adequate Logic for Full LOTOS
Muffy Calder ¹ , Savi Maharaj ² , Carron Shankland ² ( ¹ Department of Computing Science, University of Glasgow, Glasgow G12 8QQ ; ² Department of Computing Science and Mathematics, University of Stirling, Stirling FK9 4LA )

Abstract: We present a novel result for a logic for symbolic transition systems based on LOTOS processes. The logic is adequate with respect to bisimulation defined on symbolic transition systems.

16.30 - 17.00

Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics
Mícheál Mac an Airchinnigh (University of Dublin, Trinity College, Dublin, Ireland )

Abstract: The Irish School of Constructive Mathematics, which comprehends and extends the VDM, exploits an algebraic notation based upon monoids and their morphisms for the purposes of abstract modelling (of computing systems). Its method depends upon an operator calculus. It owes its origins and much of its notation to the original VDM and derivations thereof. The School hereto eschewed every form of formal language and formal logic, relying solely upon constructive (and executable) mathematics. For reference it may be considered to be a model-theoretic specification language together with a well-formulated development method in the same camp as B and Z. In the spirit of the unified theories of programming text of Tony Hoare and Hifeng Je, Cliff Jones' call for unified theories of modelling and/or specification, and the illuminating development of Milner's pi-calculus, the School is committed to the development of the modelling of computing (and in general other non-computing) systems in full generality. This shift was due primarily to research in the geometry of formal methods, initially triggered by the discovery that the tail-recursive map of the length homomorphism of the free monoid could be extended in a natural way to an affine transformation in the usual geometric sense. This contact point, albeit tenuous, was considerably elucidated by the modelling of a hash table as a (trivial) fibre bundle. From fibre bundles to sheaves was a natural step. Concurrently, the School moved from the algebra of monoids to categories, and from categories to topoi. Finally, the constructive nature of the School is now coming to terms with formalism and logic through the (natural) intuitionistic logic inherently manifest through topoi. In this paper we exhibit a suitably accessible trajectory or bridge from classical model-theoretic formal methods to the (in our considered opinion) more natural and (consequently self-evident!) universal topos-theoretic formal methods in the goal towards unification. (Keywords: cartesian closed category, constructive mathematics, education, Heyting algebra, intuitionistic logic, method, modelling, pedagogy, process calculi, specification, topos, VDM.)

17.00 - 17.30

Faithful Translations Among Models and Specifications
Shmuel Katz (Computer Science Department,The Technion, Haifa, Israel )

Abstract: Numerous translations exist between the design notations of formal methods tools, usually between two specific notations. In addition, more general translation frameworks are under development. For any translation it is vital that properties true of the semantic interpretations of the source and the translated notations are closely related.

Some possible applications of translations are first described. Then, key issues in translating among models with inconsistent features are identified, leading to a source and a target model that are closely related, but do not always preserve either the structure or the correctness of properties in a simple way. The concept is presented of a faithful relation among models and families of properties true of those models. In this framework families of properties are provided with uniform transformations, in addition to the translations of the models. Three variants are presented, depending on the intended use of the translation. This framework is shown appropriate for common instances of relations among translations previously treated in an ad hoc way. Furthermore, it allows expressing connections among models where one is neither a refinement nor an abstraction of the other. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation.

  Friday, 16th March

Session 9: Invited talk
Chair: José N. Oliveira ( University of Minho, Portugal )

9.30 - 10.30

Composing contracts: an adventure in financial engineering
Simon Peyton Jones (Microsoft Research Ltd, Cambridge CB2 3NH, England)

Abstract: Financial and insurance contracts -- options, derivatives, futures, and so on -- do not sound like promising territory for functional programming and formal semantics. To our delight, however, we have discovered that insights from programming languages bear directly on the complex subject of describing and valuing a large class of contracts.

In my talk I will introduce a combinator library that allows us to describe such contracts precisely, and a compositional denotational semantics that says what such contracts are worth. In fact, a wide range programming-language tools and concepts -- denotational semantics, equational reasoning, operational semantics, optimisation by transformation, and do on -- turn out to be useful in this new setting.

Sleep easy, though; you do not need any prior knowledge of financial engineering to understand this talk!

10.30 - 11.00

Coffee Break

Session 10: Formal techniques in system testing
Chair: John Fitzgerald ( Centre for Software Reliability, UK )

11.00 - 11.30

From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study
Manuel J. Fernández-Iglesias , Francisco J. González-Castaño , José M. Pousada-Carballo , Martín Llamas-Nistal , Alberto Romero-Feijoo (Grupo de Ingeniería de Sistemas Telemáticos. Departamento de Tecnologías de las Comunicaciones. Universidad de Vigo. Campus Universitario s/n. E-36200 Vigo, Spain )

Abstract: We describe our experience using Formal Description Techniques (FDTs) to support the design of interception systems for GSM networks. Both the GSM protocol and the interceptor have been specified using LOTOS, an FDT standardized by the International Standardization Organization (ISO) to describe communication systems and protocols. This has permitted us to assess the feasibility of the proposed system and speed up further design phases. From the LOTOS model, a simulator has been generated automatically. The TOPO tool set was used across the process. An FTPlink to a package containing the specification and the simulator is provided.

11.30 - 12.00

Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System
Laurent Arditi ¹ , Hédi Boufaïed ¹ , Arnaud Cavanié ² , Vincent Stehlé ² ( ¹ Texas Instruments. MS 21. BP 5. 06270 Villeneuve Loubet, France ; ² Simulog. Les Taissounnières, Route des Dolines. 06560 Valbonne, France )

Abstract: We propose a complete methodology for the automatic generation of test cases in the context of digital circuit validation. Our approach is based on a software model of the system to verify in which some modules are written in the Esterel language. An initial test suite is simulated and the state coverage is computed. New test sequences are automatically generated to reach the missing states. We then convert those sequences into system-level test cases (i.e. in-struction sequences) by a technique called "pipeline inversion". The method has been applied for the functional validation of an industrial DSP system giving promising results.

12.00 - 12.30

Using formal verification techniques to reduce simulation and test effort
O. Laurent ¹ , P. Michel ² , V. Wiels ² ( ¹ Aerospatiale-Matra-Airbus, A/BTE/SY/MS 316 route de Bayonne, 31000 Toulouse cedex 03, France ; ² ONERA-CERT/DTIM BP 4025, 2 avenue E. Belin, 31055 Toulouse Cedex 4, France )

Abstract: This paper describes an experiment in using formal methods in an industrial context. The goal is to use formal verification techniques in order to alleviate the simulation and test activities. The application is a flight control computer of the Airbus A340.

12.30 - 14.00

Lunch

Session 11: Case studies, tools and verification experiments
Chair: Yves Ledru ( LSR/IMAG, France )

14.00 - 14.30

Transacted Memory for Smart Cards
Pieter H. Hartel ¹ , Michael J. Butler ¹ , Eduard de Jong ² , Mark Longley ( ¹ Dept. of Electronics and Computer Science, Univ. of Southampton, UK ; ² Sun Microsystems, Inc. Palo Alto, CA 94043 USA )

Abstract: A transacted memory that is implemented using EEPROM technology offers persistence, undoability and auditing. The transacted memory system is formally specified in Z, and refined in two steps to a prototype C implementation / SPIN model. Conclusions are offered both on the transacted memory system itself and on the development process involving multiple notations and tools.

14.30 - 15.00

Houdini, an Annotation Assistant for ESC/Java
Cormac Flanagan , K. Rustan M. Leino (Compaq Systems Research Center 130 Lytton Ave., Palo Alto, CA 94301, U.S.A. )

Abstract: [ no abstract provided ]

15.00 - 15.30

A Heuristic for Symmetry Reductions with Scalarsets
Dragan Bosnacki ¹ , Dennis Dams ² , Leszek Holenderski ¹ ( ¹ Dept. of Computing Sci., Eindhoven University of Technology PO Box 513, 5600 MB Eindhoven, The Netherlands ; ² Dept. of Electrical Eng., Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands )

Abstract: We present four versions of a new heuristic for coping with the problem of finding (canonical) representatives of symmetry equivalence classes (the so-called orbit problem), in symmetry techniques for model checking. The practical implementation of such techniques hinges on appropriate workarounds of this hard problem, which is equivalent to graph isomorphism. We implemented the four strategies on top of the Spin model checker, and compared their performance on several examples, with encouraging results.

15.30 - 16.00

Coffee Break

Session 12a: Information maintenance and refactoring
Chair: Richard Moore ( UNU/IIST, Macau )

16.00 - 16.30

View Updatability Based on the Models of a Formal Specification
Michael Johnson , Robert Rosebrugh (Department of Computing, Macquarie University, Sydney, Australia Department of Computer Science, Mount Allison University, NB, Canada )

Abstract: Information system software productivity can be increased by improving the maintainability and modifiability of the software produced. This latter in turn can be achieved by the provision of comprehensive support for views, since view support allows application programs to continue to operate unchanged when the underlying information system is modified. But, supporting views depends upon a solution to the view update problem, and proposed solutions to date have only had limited, rather than comprehensive, applicability. This paper presents a new treatment of view updates for formally specified information systems. The formal specification technique we use is based on category theory and has been the basis of a number of successful major information system consultancies. We define view updates by a universal property in a subcategory of models of the formal specification, and explain why this indeed gives a comprehensive treatment of view updatability, including a solution to the view update problem. However, a definition of updatability which is based on models causes some inconvenience in applications, so we prove that in a variety of circumstances updatability is guaranteed independently of the current model. The paper is predominantly theoretical, as it develops the theoretical basis of a formal methods technique, but the methods described here are currently being used in a large consultancy for a government Department of Health. Because the application area, information systems, is rarely treated by formal methods, we include some detail about the formal methods used. In fact they are extensions of the usual category theoretic specification techniques, and the solution to the view update problem can be seen as requiring the existence of an initial model for a specification. (Keywords: View update, formal specification, information system, category theory.)

16.30 - 17.00

Transformations for Grammar Adaptation
Ralf Lämmel (CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands )

Abstract: We employ grammar transformations for the adaptation of grammars. Starting from a few fundamental grammar transformations, and some supplementary notions like focus, constraint and yielder we derive an operator suite for grammar adaptation. Three major kinds of adaptations are separated, namely transformations for refactoring, construction and destruction. While refactoring is semantics-preserving in the narrow sense, transformations for construction and destruction require the consideration of relaxed notions of semantics preservation based on other grammar relations than equality of generated languages. The consideration of semantics and accompanying preservation properties is slightly complicated by the fact that we cannot insist on reduced and terminated grammars.

A derived transformational approach to grammar improvement has been successfully applied in grammar recovery projects. More generally, the grammar adaptations covered in the paper are also useful in grammar development including maintenance.

Session 12b: Combining strategies
Chair: Peter Gorm Larsen ( IFAD, Denmark )

16.00 - 16.30

Test-Case Calculation through Abstraction
Bernhard K. Aichernig (Institute for Software Technology, Graz University of Technology, Inffeldgasse 16b, A-8010 Graz, Austria )

Abstract: This paper discusses the calculation of test-cases for interactive systems. A novel approach is presented that treats the problem of test-case synthesis as an abstraction problem. The refinement calculus is used to formulate abstraction rules for calculating correct test-case scenarios from a formal contract. This abstraction calculus results in a synthesis method that, does not need to compute a finite state machine. This is in contrast to previous work on testing from state-based specifications. A well known example from the testing literature serves to demonstrate this unusual application of the refinement calculus in order to synthesize tests rather than implementations. (Keywords: testing, test-case synthesis, refinement calculus, abstraction rules, scenarios, contract.)

16.30 - 17.00

A modular approach to the specification and validation of an Electrical Flight Control System
Marielle Doche ¹ , I. Vernier-Mounier ² , F. Kordon ² ( ¹ Dept. of Electronics and Computer Science Univ. of Southampton, Highfield Southampton SO17 1BJ, UK ; ² Laboratoire d'Informatique de Paris 6, 4 place Jussieu, F-75252 Paris Cedex 05, France )

Abstract: To study a part of an Electrical Flight Control System we have developed a tool-supported method dedicated to the incremental specification and validation of complex heterogeneous systems. Formal description of a system is structured in modules that interact. We combine two modular approaches that share the same view of modularity but offer complementary validation procedures: model checking and functional test generation. We have adapted these validation procedures to take care of the modular aspects of our specification. They are performed incrementally. We first consider basic modules, then the communication between modules and finally composed modules. To support our method, we have adapted existing tools, dedicated to non-modular specifications, to deal with modular constraints. These tools are integrated into a common platform to build a coherent execution environment. Keywords: Heterogeneous Specification, Modularity, Verification, Test Generation, Case Tools.

17.00 - 17.30

A Combined Testing and Verification Approach for Software Reliability
Natasha Sharygina ¹ , Doron Peled ² ( ¹ Robotics Research Group The Univ. of Texas at Austin Austin, TX, 78712 ; ² Bell Laboratories 600 Mountain Ave. Murray Hill, NJ, 07974 )

Abstract: Automatic and manual software verification is based on applying mathematical methods to a model of the software. Modeling is usually done manually, thus it is prone to modeling errors. This means that errors found in the model may not correspond to real errors in the code, and vice versa. In particular, if the model is found to satisfy the checked properties, the actual code may still have some errors. For this reason, it is desirable to be able to perform some consistency checks between the actual code and the model. Exhaustive consistency checks are usually not possible, for the same reason that modeling is necessary. We propose a methodology for improving the throughput of software verification by performing some consistency checks between the original code and the model, specifically, by applying software testing. In this paper we present such a combined testing and verification methodology and demonstrate how it is applied using a set of software reliability tools. We introduce the notion of a neighborhood of an error trace, consisting of a tree of execution paths, where the original error trace is one of them. Our experience with the methodology shows that traversing the neighborhood of an error was extremely useful in locating its cause. This is crucial not only in understanding where the error stems from, but in getting an initial idea of how to redesign the code. We use as a case study a robot control system, and report on several design and modeling errors found during the verification and testing process.

17.30-18.00

Closing session - End of FME 2001