| FME 2001 - List of Submitted Papers |
|---|---|
| [ FME 2001 ] |
| Accepted papers are marked red in the the following index: |
| Paper 01 |
Title: OPMSE: An Object Petri Nets based Modeling and Simulation Environment
Author(s): Luo Xueshan, Qiu Dishan, Rao Xianhong, Bao Weidong
Affiliation(s): Research Center of C3I Systems National University of Defense Technology, Changsha, Hunan, 410073 P.R.China
Date: 2000, Apr 07
File: Opmse.tar.gz
Category: unspecified
Review form: rev01.txt
Review reports: rep01.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper, the methodology of integrated simulation is proposed. The simulation conceptual framework with modeling, experiment and analysis is discussed. And an object model with integrating static, dynamic and representation characteristics is presented.
Under the direction of the above-proposed methodology, an Object Petri net-based model description language OPDL is designed and implemented. Furthermore, an integrated simulation environment OPMSE is developed. OPMSE is constituted of two packages: Model Developer and Simulator. The architecture of OPMSE is described.
Title: A Closer Look To The Cycle Derivation
Author(s): Rui Gustavo Crespo
Affiliation(s): Technical University of Lisbon, Av. Rovisco Pais, 1049001 Lisboa, Portugal
Date: 2000, Jun 21
File: FME2001.ps.gz
Category: 2
Review form: rev02.txt
Review reports: rep02.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
The mathematical construction of programs, from a given formal specification of infinite systems, is the only way to prove the correctness of the solution. In this paper we analyse the identification of different cycle instructions, based on the axiomatic basis of programming. We review the reification of the specification into one unitary cycle, and further explore the reification into more tricky instructions, such as nested cycles, sequence of cycles, and com binations of cycles and tests. At the end we highlight how can we increase the reification process productivity, by a careful selection of the derived program.
Title: From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study
Author(s): Manuel J. Fernández-Iglesias , Francisco J. González-Castaño , José M. Pousada-Carballo , Martín Llamas-Nistal , Alberto Romero-Feijoo
Affiliation(s): 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
Date: 2000, Aug 08
File: fdezvigo.ps.gz
Category: 1
Review form: rev03.txt
Review reports: rep03.txt
Comments: click here for reviewer comments about this paper (if any)
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 theInternational Standardization Organization (ISO) to describe communication systems and protocols. This has permitted us to asses the feasibility of the proposed systemand 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.
Title: Some Relations for Communication and Parallelism Elimination and Introduction on Declarative Programs
Author(s): Miquel Bertran , Francesc Babot , August Climent , Miquel Nicolau
Affiliation(s): Informàtica La Salle, Universitat Ramon Llull, Barcelona
Date: 2000, Aug 11
File: bertran.ps.gz
Category: 2
Review form: rev04.txt
Review reports: rep04.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Some congruence and refinement relations between statements of a declarative programming notation are presented. They can be used as reductions to introduce and/or eliminate synchronous communication statements and parallelism. The development is made within a restricted version of SPL, the notation for reactive programs used in the books of Manna and Pnueli, and in the Stanford Temporal Prover (STeP). However, the approach can be adapted to other declarative notations, program verifiers and model checkers. It would be a complement of these tools, deriving new programs from verifyied ones, preserving their properties, and avoiding the repetiton of verifications for related programs. The restriction affects communication statements and is unimportant for the applications. It is necessary in order to both derive the communication elimination and introduction relations, and to simplify the set of relations involving the skip statement, which are needed to apply the proper communication elimination relations. As an additional help, a nil statement is introduced in the notation. We show that no finite set of relations suffices to eliminate synchronous communication statements from programs involving the concatenation and cooperation operators only. An infinite set of relations is given to suit this purpose. However, a recursive algorithm exists for their application.
Title: Towards execution in automatic test suite generation
Author(s): Yixin Zhao , Jianping Wu
Affiliation(s): Department of Computer Science and Technology, Tsinghua University, Beijing, 100084, China
Date: 2000, Aug 14
File: post.pdf.gz
Category: 2
Review form: rev05.txt
Review reports: rep05.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Only executable test suite generated automatically has practical usage. The authors devise and implement the algorithm of "parametrizing and executizing" in the TUGEN system and discuss the result, limitation and its reason Basing on these work and the study in the executability of the transition and the satiability problem of the predicate, the authors further present and implement another algorithm called "executable parametrizing" to overcome the deficiency of the previous one and further improve the practicability and efficiency of TUGEN. After analysis and comparison, the authors outline the focus of the future research.
Title: Verifying Implementation Relations
Author(s): Jon Burton , Maciej Koutny
Affiliation(s): Department of Computing Science, University of Newcastle, Newcastle upon Tyne NE1 7RU, U.K.
Date: 2000, Aug 15
File: BK2000.ps.gz
Category: 2
Review form: rev06.txt
Review reports: rep06.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: Transacted Memory for Smart Cards
Author(s): Pieter H. Hartel , Michael J. Butler , Eduard de Jong , Mark Longley
Affiliation(s): Dept. of Electronics and Computer Science, Univ. of Southampton, UK ; Sun Microsystems, Inc. Palo Alto, CA 94043 USA
Date: 2000, Aug 17
File: memory4.ps.gz
Category: 1
Review form: rev07.txt
Review reports: rep07.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: The Development of a Computer Application that Identifies Reusable Components through Formal Specifications
Author(s): Francisco Moreira Couto
Affiliation(s): Dept. of Mathematics, Technical University of Lisbon, Portugal
Date: 2000, Aug 18
File: paper.ps.gz
Category: 2
Review form: rev08.txt
Review reports: rep08.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Software reuse is certainly a way for increasing software productivity. In this paper we propose to use Formal Methods to develop one computer application, which will be able to automate the process of software reuse. We use single-sort algebraic specifications to specify the components functionality, and then we apply the mathematical framework of category theory to develop matching mechanisms, which identify reusable components. (Keywords: algebraic specification, category theory, software reuse, specification matching.)
Title: Serialising Parallel Processes in a Hardware/Software Partitioning Context
Author(s): Leila M. Silva , Augusto Sampaio , Geraint Jones
Affiliation(s): UFS, Aracajú, Brazil ; DI-UFPE Recife, Brazil ; OUCL, Oxford, UK
Date: 2000, Aug 18
File: paperFME.ps.gz
Category: 2
Review form: rev09.txt
Review reports: rep09.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: An abstract semantics of temporal logic specifications
Author(s): Anatol Ursu
Affiliation(s): Technical University of Moldavia Computer Science Dept., bd. Stefan cel Mare 168, 2004 Chisinau, Republic of Moldavia
Date: 2000, Aug 19
File: fme2001-Ursu.ps.gz
Category: 2
Review form: rev10.txt
Review reports: rep10.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper we introduce an abstract semantics of the propositional temporal logic specifications which can be characterized by a class of deterministic Buchi automata, called abstract Buchi automata. A fixpoint characterization of the abstract semantics in the abstract Buchi automata domain is intro duced and an abstract satisfiability analysis method is proposed. An abstract interpretation is proposed which allo ws to approximate correctly the concrete semantics of temporal logic specifications by abstract Buchi automata.
Title: Business System Analysis Model with extended Entity concept
Author(s): ByungSun Ko
Affiliation(s): [ To become available very soon ]
Date: 2000, Aug 21
File: fme.pdf.gz
Category: 2
Review form: rev11.txt
Review reports: rep11.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
[ To become available very soon ]
Title: Reasoning about Failure Probabilities - formally and feasibly
Author(s): Jan Jürjens
Affiliation(s): Computing Laboratory, University of Oxford, GB
Date: 2000, Aug 21
File: probty.ps.gz
Category: 2
Review form: rev12.txt
Review reports: rep12.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
It is often not feasible to formally reason about fault-tolerant systems while keeping track of the probabilities of all possible faults that may occur during their execution. However, one may not just neglect these probabilities if one would like to show that the employed fault-tolerance components are sufficient for the required level of dependability. In the specification framework of FOCUS, we present a specification language that is interpreted firstly in an abstract model allowing formal reasoning in a feasible way. Secondly, it is interpreted in a probabilistic model. We give probability bounds that show the degree of faithfulness of the abstract model wrt. the probabilistic one. Further results are given for refinement and composition of systems.
Title: Towards a Formal Framework for Object Oriented Architecture
Author(s): Amnon H. Eden , Yoram Hirshfeld
Affiliation(s): Department of Computer Science, Concordia University, Montreal, Canada ; School of Mathematics, TelAviv University, Tel Aviv, Israel
Date: 2000, Aug 21
File: tffooa.ps.gz
Category: 1
Review form: rev13.txt
Review reports: rep13.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Architectural representations of software systems are designed to provide a concise roadmap to the elements in the system's composition and the interplay thereof. Supporting Formalisms strive to deliver a succinct expression for architectural specifications. Independently, progress was made in the understanding of OO architecture through the introduction of patterns of design and architecture. However, there is no agreement which formalism should be used to specify software architecture and architectural patterns, nor there is an agreement which are the elementary units thereof. This article presents an underlying framework for the formal specification of OO architecture: We observe building blocks in OO architectures; reformulate informal concepts in patterns of OO design and architecture; and define a universal, logic language for the representation of this knowledge. Finally, we use our conceptual toolkit to compare and evaluate proposed formalisms. (Keywords: Software architecture, object oriented programming, design patterns, tool support)
Title: Hierarchic Normal Forms for desynchronization
Author(s): Jean-Pierre Talpin , Albert Benveniste , Benoit Caillaud , Paul Le Guernic
Affiliation(s): INRIA - IRISA, Campus de Beaulieu, 35042 Rennes cedex, France
Date: 2000, Aug 23
File: fme.ps.gz
Category: 2
Review form: rev14.txt
Review reports: rep14.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
We present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. This theory can be used as a basis for correct distributed code generation. The present paper presents a new data structure, the hierarchic normal form for a transition relation, which is instrumental in implementing this theory. We illustrate this on a STATCHARTS example.
Title: A Formal Model of Object-Oriented Design and GoF Design Patterns
Author(s): Andres Flores , Richard Moore , Luis Reynoso
Affiliation(s): Department of Informatics and Statistics - University of Comahue, Buenos Aires 1400, 8300 Neuquen, Argentina ; UNU/IIST, P. O. Box 3058, Macau
Date: 2000, Aug 24
File: fme.ps.gz
Category: 1
Review form: rev15.txt
Review reports: rep15.txt
Comments: click here for reviewer comments about this paper (if any)
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 objectoriented 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 objectoriented 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.
Title: Towards a Formalization of the UML State Machine using Object-Z
Author(s): Soon-Kyeong, Kim , David Carrington
Affiliation(s): School of Computer Science and Electrical Engineering The University of Queensland, Brisbane, 4072, Australia
Date: 2000, Aug 24
File: soonfme01.ps.gz
Category: 2
Review form: rev16.txt
Review reports: rep16.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
This paper presents a formalization using Object-Z of the State Machine package in the UML metamodel. In the specification, the abstract syntax and the static and dynamic semantics for each individual model construct in the package are grouped together and encapsulated within a single Object-Z class. For formalizing the dynamic semantics, a denotational semantics of the con-struct is first given ignoring detailed operational sequences. Based on this de-notational semantics, an operational semantics is then defined in terms of (Object-Z) class operations and invariants constraining the operation sequences. The timed refinement calculus is used to define the operation sequences within Object-Z. Our approach enhances the precision of the UML state machine de-scription and overcomes the lack of modularity, extensibility and reusability of the current UML semantic representation. (Keywords: Formal Methods, Object-Z, UML semantics, UML Metamodel Formalization).
Title: Model Checking Verification of Logic Control Programs in SIPN
Author(s): Xiying Weng , Lothar Litz
Affiliation(s): Institute of Process Automation, Dept. of Electrical and Computer Engineering, University of Kaiserslautern PO 3049, D-67653 Kaiserslautern, Germany
Date: 2000, Aug 24
File: weng_litz.ps.gz
Category: 1
Review form: rev17.txt
Review reports: rep17.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Symbolic model checking is a promising verification technique for industrialapplications. In the area of automation, this technique appears also useful for verifying logic control programs. In this contribution, applying this technique to the verification of a logiccontrol program, which is described in the SIPN (Signal Interpreted Petri Net) framework, is addressed. Based on the isomorphism between Boolean algebra and the SIPN framework, aBoolean formula to represent transition relations of an SIPN is derived, so that applying symbolic model checker for verifying an SIPN program is made possible. Finally, anindustrial example is used to illustrate this approach. (Keywords: CTL, symbolic model checking, Petri net, logic control program.)
Title: Exploring Timing Properties Using VDM++
Author(s): Paul Mukherjee , Fabien Bousquet , Jérôme Delabre , Stephen Paynter , Peter Gorm Larsen
Affiliation(s): IFAD, Forskerparken 10, DK-5230, Odense M, Denmark ; Matra BAe Dynamics France, 20-22 rue Grange Dame Rose, 78141 Velizy-Villacoublay Cedex, France ; Matra BAe Dynamics (UK) Ltd, FPC 450, P.O. Box 5, Filton, Bristol, BS34 7QW
Date: 2000, Aug 24
File: paper.ps.gz
Category: 2
Review form: rev18.txt
Review reports: rep18.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
A new and unique method of timing property exploration based on the formal specification notation VDM++ is presented. It is explained how the VDM++ notation and tool support has been adapted to enable a pragmatic approach to detect potential timing bottlenecks with a software design before expensive commitment to an efficient implementation is made. The approach is explained both informally and semantically, and an example is presented.
| Paper 19 |
Title: Evaluation of B specifications using Constraint Logic Programming with sets
Author(s): Fabrice Bouquet , Bruno Legeard , Fabien Peureux , Laurent Py
Affiliation(s): Laboratoire d'Informatique Université de Franche-Comte 16, route de gray - 25030 Besançon cedex 13, France
Date: 2000, Aug 24
File: bouquet.ps.gz
Category: 1
Review form: rev19.txt
Review reports: rep19.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
This paper proposes an approach to the evaluation of B formal specifications using Constraint Logic Programming with sets. To evaluate the specifications, operations are calculated (when preconditions are checked) and invariants properties are verified on the generated states. The graph of all reachable states can be constructed. This approach is used to animate B formal specifications. This paper presents a system for constraint resolution to B formal specifications. This solver, noted CLPS-B, is described in terms of constraint domains, consistence verification and constraint propagation. The constrained state is defined, which makes possible the propagation of the non-determinism of the B specifications and the reduction of number of states in a reachable graph. We illustrate this approach by comparing the constrained states graph exploration with the concrete one in a simple example: Process scheduler. (Keywords: B Method, CLP, CSP, Set constraints, Evaluation of specifications, Animation.)
Title: An Integrated Refinement Calculus For Z
Author(s): Bing Wu , D.R.W. Holton , Luming M. Lai
Affiliation(s): University of Bradford, Bradford, BD7 1DP, West Yorkshire, UK
Date: 2000, Aug 24
File: fme01.ps.gz
Category: 2
Review form: rev20.txt
Review reports: rep20.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
After more than twenty years of research, formal methods are beginning to be used in industry. Despite theoretical progress and numerous case studies and pilot projects, adoption of formal methods by organizations has been slow, partly due to concerns about their cost, lack of tool support, and the skills required for their application. The paper proposes a more practical formal software development method by integrating the Refinement Calculus with Z, and presents a software development environment in which software can be formally specified and refined to program code. We present the concept and methodology for refining a Z specification to C code. Finally, potential theoretical and practical problems of implementing such a mechanised software development method are discussed. (Keywords: Formal methods, Z, Refinement Calculus, C, Mechanised software development)
Title: Real-Time Logic Revisited
Author(s): Stephen Paynter
Affiliation(s): Matra BAe Dynamics (UK) Ltd, Filton, Bristol, UK
Date: 2000, Aug 24
File: rtl.ps.gz
Category: 2
Review form: rev21.txt
Review reports: rep21.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Faithful Translations Among Models and Specifications
Author(s): Shmuel Katz
Affiliation(s): Computer Science Department,The Technion, Haifa, Israel
Date: 2000, Aug 24
File: faithfull.ps.gz
Category: 2
Review form: rev22.txt
Review reports: rep22.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures
Author(s): V.S. Alagary , Z. Xi
Affiliation(s): Department of Computer Science, Concordia University Montreal, Quebec H3G 1M8, Canada
Date: 2000, Aug 24
File: fme.ps.gz
Category: 2
Review form: rev23.txt
Review reports: rep23.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
The main issue in the development of agent-based architectures for E-Commerce applications is toproduce 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 col-laboration. Interactions among agents must remain secure and consistent with E-Commerce business rules. Formal modeling, and analysis of agent-based architectures promote understanding and reasoningon 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 verificationprior to committing to an implementation.
Title: Model-Checking Over Multi-Valued Logics
Author(s): Marsha Chechik , Steve Easterbrook , Victor Petrovykh
Affiliation(s): Department of Computer Science, University of Toronto Toronto ON M5S 3G4, Canada
Date: 2000, Aug 24
File: paper.pdf.gz
Category: 2
Review form: rev24.txt
Review reports: rep24.txt
Comments: click here for reviewer comments about this paper (if any)
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 reason-ing 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.
Title: Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System
Author(s): Laurent Arditi , Hédi Boufaïed , Arnaud Cavanié , Vincent Stehlé
Affiliation(s): Texas Instruments. MS 21. BP 5. 06270 Villeneuve Loubet, France ; Simulog. Les Taissounnières, Route des Dolines. 06560 Valbonne, France
Date: 2000, Aug 25
File: fme2001.pdf.gz
Category: 2
Review form: rev25.txt
Review reports: rep25.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
We propose a complete methodology for the automaticgeneration of test cases in the context of digital circuit validation. Our approach is based on a software model of the system to verify inwhich some modules are written in the Esterel language. An initial test suite is simulated and the state coverage is computed. New testsequences 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 industrialDSP system giving promising results.
Title: Patterns and Simulation Relations for Behavioural Subtyping
Author(s): Heike Wehrheim
Affiliation(s): Universität Oldenburg, Fachbereich Informatik, Postfach 2503 D-26111 Oldenburg, Germany
Date: 2000, Aug 25
File: Wehrheim.ps.gz
Category: 2
Review form: rev26.txt
Review reports: rep26.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Subtyping relations for object-oriented formalisms describe relationships between super- and subclasses which satisfy the substitutability requirement imposed on types and their subtypes. Behavioural subtyping is concerned with subtypes for active classes with an explicit dynamic behaviour, specifiable for instance by object-oriented formal methods combining state-based with behavioural formalisms. Such specification languages often have a formal semantics that composes behavioural semantics for both the behaviour and the state-based part. In this paper we develop syntactic patterns for the state-based part of a subclass which guarantee the subclass to be a behavioural subtype of its superclass by construction. Our results are similar to the ones linking data refinement in state-based methods with failure-divergence refinement in CSP. In contrast to classical data refinement, subtyping (and the simulation relations used for showing the soundness of the patterns) have to cope with additional new operations in the subclass.
Title: Formal Process Specification Language with a Refinement Capability Intended for Compositional Development of Information Systems
Author(s): Serge A. Stupnikov , Leonid A. Kalinichenko
Affiliation(s): Institute for Problems of Informatics Russian Academy of Sciences Moscow, Russia
Date: 2000, Aug 25
File: EP4.ps.gz
Category: 2
Review form: rev27.txt
Review reports: rep27.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Starting with csp2B specification facilities as the core, this paper extends AMN further with additional capabilities: sequential processes, parallel composition on arbitrary level, hiding, nondeterministic choice including general choice, assignment operator, main timing primitives of Timed CSP (delay, timeout and time prefixing). The resulting process specification language with a refinement capability is intended for compositional development of information systems. An approach for mapping of extensions of the core into AMN and algorithms of their conversion into B machines are defined.
Title: Validation of UML models thanks to Z and Lustre
Author(s): Lydie Du Bousquet , Sophie Dupuy
Affiliation(s): Laboratoire LSR-IMAG, BP 72, 38402 Saint Martin d'Hères cedex, France
Date: 2000, Aug 25
File: UML-ZLustre.ps.gz
Category: 1
Review form: rev28.txt
Review reports: rep28.txt
Comments: click here for reviewer comments about this paper (if any)
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 theworld Formal Method congress 1999 tool contest.
Title: Model Checking X-Machines: Towards Integrated Formal Development of Safety Critical Systems
Author(s): George Eleftherakis , Petros Kefalas
Affiliation(s): City Liberal Studies, Affiliated Institution of the University of Sheffield, 13 Tsimiski Str, 54624 Thessaloniki, Greece
Date: 2000, Aug 25
File: EleftherakisKefalas.pdf.gz
Category: 2
Review form: rev29.txt
Review reports: rep29.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
[ To become available very soon ]
Title: Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics
Author(s): Mícheál Mac an Airchinnigh
Affiliation(s): University of Dublin, Trinity College, Dublin, Ireland
Date: 2000, Aug 25
File: FMEpaper.pdf.gz
Category: 2
Review form: rev30.txt
Review reports: rep30.txt
Comments: click here for reviewer comments about this paper (if any)
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 comput- ing (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.)
Title: An Adequate Logic for Full LOTOS
Author(s): Muffy Calder , Savi Maharaj , Carron Shankland
Affiliation(s): Department of Computing Science, University of Glasgow, Glasgow G12 8QQ ; Department of Computing Science and Mathematics, University of Stirling, Stirling FK9 4LA
Date: 2000, Aug 25
File: fme.ps.gz
Category: 2
Review form: rev31.txt
Review reports: rep31.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Model Checking for feature Interaction Analysis: controlling state-explosion
Author(s): Muffy Calder , Alice Miller
Affiliation(s): Department of Computing Science, University of Glasgow, Glasgow, Scotland
Date: 2000, Aug 25
File: calder_miller_fme.ps.gz
Category: 1
Review form: rev32.txt
Review reports: rep32.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
[ no abstract provided ]
Title: Combining Theorem Proving and Model Checking -- A Case Study
Author(s): Dennis Dams , Dieter Hutter , Natalia Sidorova
Affiliation(s): Dept. of Electrical Eng., Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands ; German Research Center for Artificial Intelligence Stuhlsatzenhausweg 3, D-66123 Saarbruecken, Germany ; Dept. of Math. and Computer Science, Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands
Date: 2000, Aug 25
File: dhs01.ps.gz
Category: 2
Review form: rev33.txt
Review reports: rep33.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
We report on a case study on the verification of the Bounded Retransmission Protocol in which the inductive theorem prover INKA was used to justify data abstractions. These abstractions arose in building a finite-state verification model, to be submitted to a model checker. Our initial experiments led us to equip INKA with new heuristics, after which the proofs went through without user interaction. We discuss the idea behind these heuristics and argue why we expect them to work as well in other cases of data abstractions.
Title: Reformulation: a Way to Combine Dynamic Properties and B Refinement
Author(s): F. Bellegarde , C. Darlot , J. Julliand , O. Kouchnarenko
Affiliation(s): Laboratoire d'Informatique de l'Université de Franche-Comté 16, route de Gray , 25030 Besançon Cedex
Date: 2000, Aug 25
File: reformulation.ps.gz
Category: 2
Review form: rev34.txt
Review reports: rep34.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: From CSP to B: Specifications of a Post Office
Author(s): Marielle Doche , Andrew Gravell
Affiliation(s): Department of Electronics and Computer Science, University of Southampton, Highfield, Southampton SO17 1BJ, United Kingdom
Date: 2000, Aug 25
File: fme01.pdf.gz
Category: 2
Review form: rev35.txt
Review reports: rep35.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper, we describe the methodology followed to specify a distributed system. The first step of this approach is to use a model checker to define a specification in CSP, which highlights the structure of the system and how the different components communicate. Then, we translate this specification in B to improve it with more complex data structures, infinite types and additional operations. Finally, we propose an approach to reuse the results of failures-divergences refinement from our CSP specification, to check data refinement of the improved B specification.
Title: A Method for Systematic Requirements Elicitation: Application to a Light Control System
Author(s): Jeanine Souquières , Maritta Heisel
Affiliation(s): LORIA-Université Nancy2, B.P. 239 Bâtiment LORIA, F-54506 Vandoeuvre-les-Nancy ; Fakultät für Informatik, Universität Magdeburg, D-39016 Magdeburg
Date: 2000, Aug 25
File: fme01.ps.gz
Category: 1
Review form: rev36.txt
Review reports: rep36.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
This paper demonstrates the use of a systematic approach to clarify and analyze the requirements of a light control system. The method includes a formalization of the requirements and the analysis of interactions between them.
Title: Debugging a Real-life Protocol with CFFD-Based Verification Tools
Author(s): Antti Kervinen , Antti Valmari , Risto Järnström
Affiliation(s): Tampere University of Technology, Software Systems Laboratory PO Box 553, FIN-33101 Tampere, Finland ; Instrumentointi Oy Sarankulmankatu 20, FIN-33900 Tampere, Finland
Date: 2000, Aug 25
File: uusiversio.ps.gz
Category: 1
Review form: rev37.txt
Review reports: rep37.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper the use of a set of verification tools, developed at the Softw are Systems Laboratory, in a real-life protocol design project is described. First, the CFFD theory, in which the toolset is based on, is taken a quick look at, and the methods used in the analysis are discussed. Then the behaviour of theprotocol is presented to the extent needed to follow the discussion on the modelling phases, and on the errors that were found. Each modelling phase, the analysis results from it, and their effects to the design of the protocol are discussed. Abstracted global behaviours of all the models of the protocol were examined visually with the help of a visualisation tool. Visualisation gave answers to verification questions like "How does the protocol behave from this point of view?" instead of the ordinary "Does the protocol beha ve like this?". This was a great advantage in finding the causes of erroneous behaviour.
Title: A synchronous model of the IEC 61131 PLC languages FBD and ST in Signal
Author(s): Fernando Jiménez-Fraustro , Éric Rutten
Affiliation(s): EP-ATR Group, IRISA, F-35042, Rennes, France ; BIP Group, INRIA Rhône-Alpes, F-38330 MONTBONNOT, France
Date: 2000, Aug 25
File: iec2sig.ps.gz
Category: 1
Review form: rev38.txt
Review reports: rep38.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
Industrial control systems feature real-time programs embedded in a variety of machines and processes, showing complexity and safety criticality. Standardization has led to the definition of the IEC 61131 design standard for Programmable Logic Controllers (PLCs). Its formalization for purposes of analysis and tool support is an active research topic. The synchronous approach to real-time and reactive systems has resulted in formalisms and effective tools for the compilation, analysis and verification of specifications. With the motivation to give access to these formal techniques and tools, this paper presents a synchronous model of the PLC programming languages ST and FBD, and of the Program Organization Units (POU), based on the language SIGNAL. (Keywords: programmable logic controllers, IEC 61131 standard, formal model, synchronous languages, Signal, tool support.)
Title: Formal Implementation of a Verification Algorithm using the B Method
Author(s): Ludovic Casset
Affiliation(s): Gemplus Research Laboratory, Av. Du Pic de Bertagne, 13881 Gémenos Cedex BP 100
Date: 2000, Aug 25
File: fme2001.ps.gz
Category: 1
Review form: rev39.txt
Review reports: rep39.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
The Java security policy is implemented by security components such as the Java Virtual Machine(JVM), the API, the verifier, the loader. It is then of prime importance to ensure that the implementation of these components is in accordance with their specification. Formal methods are used to bring themathematical proof that the implementation of these components corresponds to their specification. In this paper, the formal implementation of a verification algorithm is provided and entirely proved. It is acontinuing work on the model of a byte code verifier. The specification and the implementation is realized with the B method and its associated B0 language. The work focuses on the design and the proof of loops thatare a main problem to obtain a proved implementation.
Title: Components, Contracts, and Connectors for the Unified Modelling Language UML
Author(s): Claus Pahl
Affiliation(s): School of Computer Applications, Dublin City University, Dublin 9, Ireland
Date: 2000, Aug 25
File: fme.ps.gz
Category: 2
Review form: rev40.txt
Review reports: rep40.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Translation Validation of Optimizing Compilers by Computational Induction
Author(s): Amir Pnueli , Lenore Zuck , Paritosh Pandya
Affiliation(s): Department of Computer Science, The Weizmann Institute of Science ; Department of Computer Science, New York University ; Computer Science Group, Tata Institute of Fundamental Research, Homi Bhabha Road, Colaba, Mumbai 400 005 India
Date: 2000, Aug 25
File: fme.ps.gz
Category: 2
Review form: rev41.txt
Review reports: rep41.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
[ no abstract provided ]
Title: A Combined Testing and Verification Approach for Software Reliability
Author(s): Natasha Sharygina , Doron Peled
Affiliation(s): Robotics Research Group The Univ. of Texas at Austin Austin, TX, 78712 ; Bell Laboratories 600 Mountain Ave. Murray Hill, NJ, 07974
Date: 2000, Aug 25
File: FME2001.ps.gz
Category: 1
Review form: rev42.txt
Review reports: rep42.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Reachability Analysis of Timed Automata in Polynomial Time
Author(s): Dirk Beyer
Affiliation(s): Software Systems Engineering Research Group, Technical University Cottbus, D-03013 Cottbus, Postfach 10 13 44, Germany
Date: 2000, Aug 25
File: Reachability.ps.gz
Category: 1
Review form: rev43.txt
Review reports: rep43.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: How to Make FDR Spin LTL Model Checking of CSP by Refinement
Author(s): Michael Leuschel , Thierry Massart , Andrew Currie
Affiliation(s): 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
Date: 2000, Aug 25
File: ltl-fdr-fme2001.tex.ps.gz
Category: 2
Review form: rev44.txt
Review reports: rep44.txt
Comments: click here for reviewer comments about this paper (if any)
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 chec king (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.
Title: Avoiding State Explosion for Distributed Systems with Timestamps
Author(s): Fabrice Derepas , Paul Gastin , David Plainfossé
Affiliation(s): 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
Date: 2000, Aug 25
File: fderepas.ps.gz
Category: 2
Review form: rev45.txt
Review reports: rep45.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: Formal specification for a mathematics-based application domain: geometric modeling
Author(s): Franck Ledoux , Jean-Marc Mota , Agnès Arnould , Catherine Dubois , Pascale Le Gall , Yves Bertrand
Affiliation(s): L.a.M.I., Université d'Évry val d'Essonne, Cours Monseigneur Roméro, 91025 Evry Cedex, France. ; IRCOM-SIC, UMR 6615, Université de Poitiers, SP2MI, 86962 Futuroscope Cedex, France.
Date: 2000, Aug 25
File: article.ps.gz
Category: 1
Review form: rev46.txt
Review reports: rep46.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper, we discuss the use of formal methods in the domain of geometric modeling. More precisely, the purpose of our work is to provide a formal specification language convenient for geometric modeling with tools. To do it, we are interested in a high-level operation, the chamfering which is already mathematically defined. Then we propose two specifications of it, using the two languages B and Casl, respectively representative of model-oriented approach and property-oriented approach. In order to as well as possible take advantage of the B and Casl characteristics, we explicitly specify the chamfering in B and implicitly in Casl. In both cases, we succeeded in providing a specification easily understandable by the experts of the application domain. (Keywords: Formal specifications, B, B method, algebraic specifications, Casl, geometric modeling, n-dimensional generalized maps, chamfering.)
Title: Specification and Formal Analysis of the Light Control Problem by an integrated formal approach
Author(s): J. Christian Attiogbé
Affiliation(s): IRIN - Université de Nantes 2, rue de la Houssinière - 44322 Nantes Cedex 3
Date: 2000, Aug 25
File: lcs_fme.ps.gz
Category: 1
Review form: rev47.txt
Review reports: rep47.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
A stepwise analysis of the Light Control Problem is presented using the Configuration Machines Formalism, an integrated approach to deal with data and behavior. The result is a specification of the main parts of the Light Control System to be developed. The specification is a set of communicating machines which correspond to the subsystems identified in the Light Control System. Machines capture both data and behavior of different parts of the system. The data part of each machine is specified using Z like formalism whereas the behavior part is specified as a Labelled Transition System. Communications between machines, between machines and environment are based on synchronous message exchanges. The specification obtained is then used for formal analysis: validation of the specification by proving some properties extracted from the requirements, simulation issue is addressed by presenting a technique to translate the specification into Promela in order to use the Spin environment. (Keywords: Requirements Capture, Formal specification techniques, Configuration Machines, embedded software, Z/Eves, Promela.)
Title: A Heuristic for Symmetry Reductions with Scalarsets
Author(s): Dragan Boshnachki , Dennis Dams , Leszek Holenderski
Affiliation(s): 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
Date: 2000, Aug 25
File: symspin.ps.gz
Category: 2
Review form: rev48.txt
Review reports: rep48.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: From CSP-OZ to Java with Processes
Author(s): Ana Cavalcanti , Augusto Sampaio
Affiliation(s): Centro de Informática/UFPE P.O. Box 7851 50740-540 Recife PE Brazil
Date: 2000, Aug 25
File: fmepaper.ps.gz
Category: 2
Review form: rev49.txt
Review reports: rep49.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
The language CSP-OZ has been proposed as a combination of the more traditional specification languages CSP and Object-Z, with the objective of facilitating the definition of state and communication aspects of concurrent systems. As a conservative extension of CSP and Z, CSP-OZ is appealing to the users of these languages. In this paper we present rules that support a transformational approach to the development of concurrent Java programs from CSP-OZ specifications. Even though Java is a very successful language, its facilities for communication are very restricted and we make use of a library that supports the use of the concept of processes when writing Java programs. Our work is based on an existing refinement calculus for Z, but includes novel rules to deal with classes and CSP processes. (Keywords: formal methods, program development, refinement laws, object-orientation.)
Title: Protected Import in Modular VDM: Towards a Coadaptation of Closed and Open Views of Modules in a Structured Specification
Author(s): Theo Dimitrakos , Juan Bicarregui , Brian Matthews , Brian Ritchie
Affiliation(s): ISE Group, CLRC Rutherford Appleton Laboratory, OXON, OX11 OQX, U.K.
Date: 2000, Aug 25
File: vdm-modules-fme.ps.gz
Category: unspecified
Review form: rev50.txt
Review reports: rep50.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
The complexities and the dynamics of evolving software development today require more than ever the provision of reusable building blocks and structuring methods in order to build larger and more complex specifications. This is the first in a series of papers towards a compositional semantics for modular structured VDM specifications. We provide a compositional extension of the denotational semantics for the flat VDM-SL, emphasising on contextual structuring. In addition, we discuss some non-interference and compositionality assumptions that underlie the structuring mechanisms of modular VDM specifications and introduce a new structuring assembly called protected import in order to control information flow in contextual structuring.
Title: vdmML: using XML to represent VDM on the Web.
Author(s): Brian M. Matthews
Affiliation(s): Information Technology Department, CLRC Rutherford Appleton Laboratory, Chilton, Didcot, Oxfordshire, OX11 OQX, UK.
Date: 2000, Aug 25
File: vdmml.ps.gz
Category: 2
Review form: rev51.txt
Review reports: rep51.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper we describe some initial investigations into the use XML to support the use of VDM. This presents a snapshot of ongoing work-in-progress, and thoughts to the future development of such work, including transformationinto different formats, proof obligation generation, and integration with other formal and semi-formal methods.
Title: Information Flow Control and Applications - Bridging A Gap -
Author(s): Heiko Mantel
Affiliation(s): German Research Center for Artificial Intelligence (DFKI), Stuhlsatzenhausweg 3, D-66123 Saarbruecken, Germany
Date: 2000, Aug 25
File: mantel_2001_fme.ps.gz
Category: 2
Review form: rev52.txt
Review reports: rep52.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Houdini, an Annotation Assistant for ESC/Java
Author(s): Cormac Flanagan , K. Rustan M. Leino
Affiliation(s): Compaq Systems Research Center 130 Lytton Ave., Palo Alto, CA 94301, U.S.A.
Date: 2000, Aug 25
File: krml100.ps.gz
Category: 2
Review form: rev53.txt
Review reports: rep53.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
[ no abstract provided ]
Title: Extending the UML for Managing the Software Architecture Landscape in a Large Enterprise
Author(s): Christian Jänsch , Christoph Maier , Thomas Tensi
Affiliation(s): Cortex Brainware GmbH, Kirchplatz 5, D-82049 Pullach ; Bayerische Landesbank, Briennerstrasse 20, D-80333 Mueunchen ; sd&mAG, Thomas-Dehler-Strasse 27, D-81737 Muenchen
Date: 2000, Aug 25
File: arcus.pdf.gz
Category: 1
Review form: rev54.txt
Review reports: rep54.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In large enterprises the number of software systems for diverse tasks is very high. They have differenttechnical platforms and design philosophies but nevertheless are intensely connected. Hence to deal with the complexity of such a application network some software architecture management isnecessary.
The ARCUS method in the Bayerische Landesbank extends the Unified Modelling Language formodelling the architecture of a complete landscape of software. This is achieved by extending the UML metamodel with new stereotypes and constraints and by introduction of new notions like e.g. thederived relations. To implement this method tools are vital, but also new roles within the organisation have to be established.
Title: View Updatability Based on the Models of a Formal Specification
Author(s): Michael Johnson , Robert Rosebrugh
Affiliation(s): Department of Computing, Macquarie University, Sydney, Australia Department of Computer Science, Mount Allison University, NB, Canada
Date: 2000, Aug 25
File: fme006.ps.gz
Category: 2
Review form: rev55.txt
Review reports: rep55.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: Test-Case Calculation through Abstraction
Author(s): Bernhard K. Aichernig
Affiliation(s): Institute for Software Technology, Graz University of Technology, Inffeldgasse 16b, A-8010 Graz, Austria
Date: 2000, Aug 26
File: fme01.ps.gz
Category: 2
Review form: rev56.txt
Review reports: rep56.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: Metrics for Test Plan on Object-Oriented Behavioral Design
Author(s): Young Chul Robert Kim , C. Robert Carlson
Affiliation(s): Embedded System Lab LG Industrial System R&D Center ; Department of Computer Science, Illinois Institute of Technology, Chicago, IL 60616, USA
Date: 2000, Aug 26
File: kim.ps.gz
Category: 2
Review form: rev57.txt
Review reports: rep57.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
This paper describes a design driven approach to test plan generation. Its foundation is an object-oriented software design approach which partitions design schema into a layered architecture of functional components called "design units". A use case software development methodology is employed which preserves this unit architecture on through to the actual code structure. Based on the partition design schema produced during the design phase of this methodology, a test plan is generated which includes a set of unit and scenario based tests. A software metric is introduced which produces an ordering of this set to enhance productivity and both promote and capitalize on test case reusability. This paper contains an application which illustrates the proposed approach.
Title: An Integrated Approach to Specification and Validation of Real-Time Systems
Author(s): Adnan Sherif , Augusto Sampaio , Sérgio Cavalcante
Affiliation(s): Federal University of Pernambuco Center of Informatics P.O. BOX 7851 Cidade Universitaria 50740-540 Recife - PE Brazil
Date: 2000, Aug 26
File: sscFME2001.ps.gz
Category: 2
Review form: rev58.txt
Review reports: rep58.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Secrecy-preserving Refinement
Author(s): Jan Jürjens
Affiliation(s): Computing Laboratory, University of Oxford, GB
Date: 2000, Aug 27
File: refsec.ps.gz
Category: 2
Review form: rev59.txt
Review reports: rep59.txt
Comments: click here for reviewer comments about this paper (if any)
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 follo ws 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.
Title: Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries
Author(s): Steffen Helke , Thomas Santen
Affiliation(s): Technische Universität at Berlin Institut für Kommunikations und Softwaretechnik FR 5-6, Franklinstrasse 28/29, D-10587 Berlin
Date: 2000, Aug 27
File: fme2001.ps.gz
Category: 1
Review form: rev60.txt
Review reports: rep60.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Translation of CORBA IDL to Z
Author(s): Chris Taylor , Eerke Boiten , John Derrick
Affiliation(s): Computing Laboratory, University of Kent, Canterbury, CT2 7NF, UK
Date: 2000, Aug 28
File: idl.ps.gz
Category: 2
Review form: rev61.txt
Review reports: rep61.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
We provide a translation from CORBA IDL to the Z specification notation. Our main motivation is to integrate CORBA IDL into an existing multi-language framework for viewpoint specification and consistency checking. However, the translation could also serve as the basis for a reverse translation from a subset of Z into IDL, and for a translation into Z from IDL specifications augmented with Z annotations that express behavioural constraints not expressible in IDL itself. (Keywords: CORBA IDL, Z, translation, specification languages, signatures, viewpoints, consistency.)
Title: Integration of Control and Datatypes using the View Formalism
Author(s): Christine Choppy , Pascal Poizat , Jean-Claude Royer
Affiliation(s): LIPN, Institut Galilé - Université Paris XIII, Avenue Jean-Baptiste Clément, F-93430 Villetaneuse, France ; IRIN, Université de Nantes 2 rue de la Houssinière, B.P. 92208, F-44322 Nantes cedex 3, France
Date: 2000, Aug 25
File: fme.ps.gz
Category: 2
Review form: rev62.txt
Review reports: rep62.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper we present a specification formalism that provides a coherent framework for the integration of static and dynamic aspects of a system. In our approach, a system is specified as the composition of several components. Our framework is based on the concept of view which is a formal structure used to describe the static and dynamic parts of a component and their integration. Views are also the structuring mechanism for components. Each basic component has two views, a dynamic and a static view. Those two views are glued together by axioms and temporal logic formulas.
Our formalism uses Symbolic Transition Systems (STS) [10], a kind of guarded state/transition diagrams that finitely represent potentially infinite systems, to increase the readability and abstraction of the specification. The STS diagrams are an alternative to the textual representation of operations in terms of pre/post-conditions.
The system is structured by means of collections of objects (with identities). Axioms and temporal logic formulas are again used to glue the components altogether and express a generalized form of synchronous product [2].
We show how a global view structure may then be retrieved.
The formalism is explained using a simplified phone service example.
Title: A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware
Author(s): Nalini Venkatasubramanian , Carolyn Talcott , Gul Aghaz
Affiliation(s): 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
Date: 2000, Aug 28
File: fme2001submit.ps.gz
Category: 2
Review form: rev63.txt
Review reports: rep63.txt
Comments: click here for reviewer comments about this paper (if any)
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.)
Title: Proofs of Correctness of Cache-Coherence Protocols
Author(s): Joseph Stoy , Xiaowei Shen , Arvind
Affiliation(s): MIT Laboratory for Computer Science, 545 Technology Square,Cambridge Ma 02139 USA
Date: 2000, Aug 20
File: fme.ps.gz
Category: 1
Review form: rev64.txt
Review reports: rep64.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Transformations for Grammar Adaptation
Author(s): Ralf Lämmel
Affiliation(s): CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands
Date: 2000, Aug 30
File: stfga.ps.gz
Category: 2
Review form: rev65.txt
Review reports: rep65.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Using formal verification techniques to reduce simulation and test effort
Author(s): O. Laurent , P. Michel , V. Wiels
Affiliation(s): 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
Date: 2000, Aug 25
File: fme01.ps.gz
Category: 1
Review form: rev66.txt
Review reports: rep66.txt
Comments: click here for reviewer comments about this paper (if any)
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.
Title: Model Checking Safety Critical Systems
Author(s): C. Bernardeschi , Alessandro Fantechi , S. Gnesi
Affiliation(s): Dip. di Sistemi e Informatica, Univ. di Firenze, Italy ; Istituto di Elaborazione dell'Informazione, C.N.R. Pisa, Italy ; Dipartimento di Ingegneria della Informazione, Univ. di Pisa, Italy
Date: 2000, Aug 31
File: fmsafes5.ps.gz
Category: 1
Review form: rev67.txt
Review reports: rep67.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
In this paper we argue that safety critical systems are the next candidate to share the success that formal verification techniques based on model checking are enjoying in the field of hardware verification. We motivate this statement first reviewing how formal methods have so far been applied in the development of safety critical systems, and then discussing the critical points for the success of the introduction of formal methods in such a field. The results presented in this paper are based on our experience of formal verification of fault-tolerant safety critical systems by means of model checking techniques. In particular we show how fault tolerant systems posses some characteristics that help in limiting the "state explosion problem" when model checking algorithms are used on industrial cases studies.
Title: The Temporal Logic of Distributed Actions
Author(s): Wolfgang Reisig , Adrianna Foremniak
Affiliation(s): Humboldt-Universität zu Berlin, Germany
Date: 2000, Aug 25
File: tlda.ps.gz
Category: 2
Review form: rev68.txt
Review reports: rep68.txt
Comments: click here for reviewer comments about this paper (if any)
Abstract:
We reformulate Lamport's TLA to cope with Distributed Actions. Temporal Logic of Distributed Actions (TLDA) retains all valuable properties of TLA (such as "implementation is implication" and "composition is conjunction"). TLDA can express important properties of Distributed Systems that can not be expressed in TLA. In particular, the notion of progress replaces the conventional, but less adequate notion of weak fairness. Finally, we challenge Lamport's arguments about concurrent runs.
Title: A Generic Functional Framework for Developing Genetic Algorithm
Author(s): John Hawkins, Ali Abdallah
Affiliation(s): Centre of Applied Formal Methods South Bank University 102 Borough Road, London, UK
Date: 2000, Sep 03
File: ga_fme.ps.gz
Category: unspecified
Comments: late submission
Abstract:
Almost all genetic algorithms are different instances of a single skeleton which is neatly expressed as a higher order function in Haskell. This paper is intended to give a brief overview of evolutionary computation and to present a general functional framework for developing genetic algorithms (GAs). This is mainly centered around a generic functional GA skeleton and a rich library for instantiating its components. The usefulness of this framework is demonstrated by considering four different computationally complex problems and developing GA solutions to these problems within the functional framework.
Title: Algebraic Identities for Pipelining Higher Order Functions
Author(s): Ali Abdallah
Affiliation(s): The University of Reading Department of Computer Science Reading, RG6 6AY, UK
Date: 2000, Sep 03
File: ali2.ps.gz
Category: unspecified
Comments: late submission
Abstract:
A calculus of function decompositions for parallel programs derivation based on Bird-Meertens Formalism is presented. This is mainly a collection of useful algebraic identities between forms of algorithmic expressions. The main focus is on highlighting the algebra of a compositional functional form known as a pipe pattern. This functional form is suitable for highly parallel implementations. We show how this form can be systematically refined into pipelined networks of communicating processes in Hoare's CSP. It turns out that all familiar higher order functions such as map, filter, foldl, and foldr can be identitied with new algorithmic forms expressed as instances of this pipe pattern. This greatly facilitates a transformational programming methodology for deriving pipelining algorithms from abstract functional specifications. A catalogue of useful algebraic transformation rules which allow the decomposition of higher order functions to be derived from the decomposition of their arguments is presented. Novel methods for parallelizing directed reduction when the operator involved is not associative are developed. We show how the calculus can be applied for deriving highly parallel solutions to a variety of problems.
Title: KICKER: A Decision Support Tool For Multi-modal Traffic Based on Multi-agent Systems
Author(s): Alessio Cuppari, Pier Luigi Guida, Maurizio Martelli, Floriano Zini
Affiliation(s): Sistemi Informativi, Divisione Infrastrutture - FS S.p.A. P.zza Croce Rossa 1, 00161 Roma, Italy
Date: 2000, Sep 06
File: kicker.ps.gz
Category: 1
Comments: late submission
Abstract:
KICKER is a joint project between the Information Systems Division of Italian Railways (FS S.p.A.) and the Computer Science Department at the University of Genova, Italy. It is based on the results of the EuROPE-TRIS project (Guida, 1998) and its aim is to realize a decision support system to be used by train control co-ordinators, working along European lines, in the management of freight trains traffic towards multi-modal centres of shipment. The realization of KICKER is carried out using CaseLP, a prototyping environment for software applications modelled as Multi-Agent Systems. CaseLP combines well established prototyping techniques, based on traditional software engineering approaches with the innovative paradigm of Multi-Agent Systems, that suits very well the realization of distributed, dynamic and heterogeneous software applications. The paper outlines the KICKER project, presents the principal features of CaseLP and summarizes the results that have been obtained till now. Keywords: Agents, Decision support systems, Prototyping, Traffic control
| Paper 72 |
Title: Modular approach to specify and validate an Electrical Flight Control System
Author(s): Marielle Doche , I. Vernier-Mounier , F. Kordon
Affiliation(s): 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
Date: 2000, Jul 25
File: FME_Mounier.ps
Category: 1
Review form: rev72.txt
Review reports: rep72.txt
Comments: click here for reviewer comments about this paper (if any)
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.