Virtual Library
Formal Methods
Meetings
Virtual Library
Formal Methods
Meetings
![[Audio welcome]](/archive/sound/sound-icon.gif){kind=icon}
Date:
Thursday, April 6, 1995 (5:30pm to 8pm)
Venue:
Computer Science and Engineering Department,
Florida Atlantic University
FDR (Failures-Divergence Refinement) is a software package which allows the automatic checking of many properties of finite state systems and the interactive investigation of processes which fail these checks. It is based on the mathematical theory of Communicating Sequential Processes (CSP), developed at Oxford University and subsequently applied successfully in a number of industrial applications. Systems with 10**7 states can be analysed in minutes on a standard low-end workstation. Unlike most packages of this type, FDR was specifically developed for industrial applications, in the first instance at Inmos where it is used to develop and verify communications hardware. Therefore it is constructed to make its capabilities understandable and usable, and has extensive debugging facilities to allow system development, rather than simply verification. Existing and potential applications include VLSI design, protocol development and implementation, networking and data distribution, control, signalling, fault-tolerant systems, telecommunications and man-machine interface.
FDR supports reasoning about communicating systems of finite-state processes using the untimed theory of CSP, where we are interested in the order, but not exact times, of events. The theory of refinement in CSP allows most correctness conditions (safety and liveness, but not fairness in the current version) to be encoded as the most nondeterministic process satisfying them. We can test whether an implementation meets the specification by deciding if it refines the specification process. FDR is therefore built around this decision question. It implements a normalisation procedure for the specification process, which represents the specification in a form where the implementation can be checked against it by model-checking techniques (exploring reachable states). Both the specification and the implementation must therefore be finite-state processes.
Because FDR is designed for the development of systems which have complex behaviour. Frequently a first attempt at an implementation will fail to meet its specification, and it is vital that the system developer has the means to understand why. When a refinement check fails, FDR provides the means to explore the way the error arose. It allows the user to explore the state of the implementation, and its subprocesses at the point where the error was detected, and during the prior evolution of the system.
David Jackson,
Formal Systems (Europe) Ltd
3 Alfred Street
Oxford OX1 4EH
UKTel: +44 (0)1865 728460
Fax: +44 (0)1865 201114
E-mail: dave@fsel.com
----------------------------------------------------------------------- | Item | Requirements | |==================|==================================================| | Platform | Sun-4 (SPARC) | HP 9000/700 series | |------------------|-----------------------|--------------------------| | Operating system | Sun-OS 4.1 or | HP-UX version 9 | | | Solaris 2.3 | | |------------------|--------------------------------------------------| | Window | OSF Motif 1.1 or | | management | OpenWindows version 2 or 3 (Sun-4 platform only) | |------------------|--------------------------------------------------| | Internal memory | Minimum 16 Mbytes | |------------------|--------------------------------------------------| | Swap space | Minimum 25 Mbytes | |------------------|--------------------------------------------------| | Disk space | Minimum 25 Mbytes | |------------------|--------------------------------------------------| | Installation | DC 6150 data cartridge tapes or | | device needed | Exabyte cartridges (112 m) or | | | FTP connection (VPP only) | -----------------------------------------------------------------------
Mr. Philippe Leblancor from:
Verilog S.A.
150 rue Nicolas Vauquelin
B.P. 1310
31106 Toulouse Cedex
FRANCETel: +33-61-192939
Fax: +33-61-408452
E-mail: leblanc@verilog.fr
Mr. Henrik Voss
IFAD
Forskerparken 10
5230 Odense M
DENMARKTel: +45-63-157131
Fax: +45-65-932999
E-mail: toolbox@ifad.dk
Cabernet is available free of charge since the beginning of 1994. More than 30 licences have been signed so far by universities, research institutions and private companies located in Europe, US, Canada, Central and South America, Japan. Cabernet has been validated on several case-studies provided by independent institutions. The most notable case-studies are: a gas burner, proposed in the literature, a node of an electrica switching network, proposed by the Italian Electricity Company, the control system of a robot arm, proposed by ESA, the control system of a railway crossing, proposed as working example for IWSSD94.
Cabernet is now background of an ESPRIT project (IDERS), that aims at building commercial tools based on the most innovative ideas that can find immediate success n the market. In particular the customization and animation components should be implemented to enhance Software through Picture, one of the main commercial tools that support the development of real-time systems.
Cabernet is available via anonymous FTP from ftp-se.elet.polimi.it: executable code, manuals, and related documentation are provided.
Professor Mauro Pezzé
Dipartimento di Elettronica
Politecnico di Milano
Piazza Leonardo da Vinci 32
20133 Milano
ITALYTel: +39-2-2399-3523
Fax: +39-2-2399-3411
E-mail: pezze@elet.polimi.it
The Vienna Development Method (VDM) is one of the most mature formal methods, primarily intended for the formal specification and the subsequent development of functional aspects of software systems. A central element of VDM is its specification language: VDM-SL.
VDM-SL is a formal specification language which is used during the specification and design phases of a software development project and supports the production of correct and high quality software. Compared to traditional textual specifications, a formal specification is unambiguous and can be automatically checked for many inconsistencies and errors. Using the high-level constructs offered by VDM-SL a specification can be described formally without dealing with implementation details.
VDM-SL is a wide spectrum specification language: it can be used for both highly abstract specifications and for specifications at a very low level of abstraction, and it supports both functional and imperative specification styles.
VDM-SL is being standardised under the auspices of the International Standards Institution (ISO) and the British Standards Institution (BSI). The standard is expected to become finally accepted in 1994.
In order to test a specification it is necessary to be able to execute it, and the Toolbox therefore supports both execution and debugging facilities for all executable constructs in VDM-SL. The test coverage tool enables the specifier to see how well a test suite covers the specification by displaying the parts of the specification which have not been executed during the test.
The test suites which were used to test the specification, can often be re-used when testing the implementation. This will help to ensure a correct transformation from the specification into an implementation.
The Toolbox supports:
All the tools in the IFAD VDM-SL Toolbox are integrated through an interface to the GNU Emacs text editor but they are also available as Unix command-line tools.
One of the benefits of executing specifications is that testing techniques can be used to assist validation of the specifications. In the development process small examples for parts of a specification can be executed to enhance the designer's knowledge of, and confidence in the specification. Furthermore an executable specification can form a running prototype.
The test coverage information is displayed directly in the source-file, in a comprehensive form which is easy to read.
Peter Gorm Larsen
IFAD
Forskerparken 10
5230 Odense M
DENMARKTel: +45 63 15 71 31
Fax: +45 65 93 29 99
E-mail: toolbox@ifad.dk
Computer Science Laboratory
SRI International
Menlo Park, CA, USA
pvs-request@csl.sri.com
PVS provides mechanized support for formal specification and verification. It builds on over 15 years experience at SRI in building and using tools to support formal methods, and we believe you will find it among the most effective verification systems for several classes of applications. The system is freely available under license from SRI and has been installed at over 30 sites in North America, Europe, and Asia.
PVS consists of a specification language, a number of predefined theories, a theorem prover, various utilities, documentation, and several examples that illustrate different methods of using the system in several application areas. PVS exploits the synergy between a highly expressive specification language and powerful automated deduction; for example, some elements of the specification language are made possible because the typechecker can use theorem proving. This distinguishing feature of PVS has allowed perspicuous and efficient treatment of many examples that are considered difficult for other verification systems.
The specification language of PVS is based on classical, typed higher-order logic. The base types include uninterpreted types that may be introduced by the user, and built-in types such as the booleans, integers, reals, and the ordinals up to epsilon_0; the type-constructors include functions, sets, tuples, records, enumerations, and recursively-defined abstract data types. Predicate subtypes and dependent types can be used to introduce constraints, such as the type of prime numbers. These constrained types may incur proof obligations during typechecking, but greatly increase the expressiveness and naturalness of specifications. In practice, most of the obligations are discharged automatically by the theorem prover. PVS specifications are organized into parameterized theories that may contain assumptions, definitions, axioms, and theorems. Definitions are guaranteed to provide conservative extension; to ensure this, recursive function definitions generate proof obligations. PVS expressions provide the usual arithmetic and logical operators, function application, lambda abstraction, and quantifiers, within a natural syntax. Names may be freely overloaded, including those of the built-in operators such as AND and +.
The PVS theorem prover provides a collection of powerful primitive inference procedures that are applied interactively under user guidance. The primitive inferences include propositional and quantifier rules, induction, rewriting, and decision procedures for linear arithmetic. User-defined procedures can combine these primitive inferences to yield higher-level proof strategies. Proofs yield scripts that can be edited, attached to additional formulas, and rerun. This allows many similar theorems to be proved efficiently, permits proofs to be adjusted economically to follow changes in requirements or design, and encourages the development of readable proofs.
PVS uses GNU Emacs to provide an integrated interface to its specification language and prover, and provides many status-reporting and browsing tools, as well as the ability to generate typeset specifications (in user-defined notation) using LaTeX.
PVS is mainly intended for the formalization of requirements and design-level specifications, and for the analysis of intricate and difficult problems. It (and its predecessors) have been chiefly applied to algorithms and architectures for fault-tolerant flight control systems, and to problems in hardware and real-time system design. Several examples are described in papers available from the SRI Formal Methods WWW page. Recent work has developed PVS methodologies for hardware verification (including integration with a BDD-based decision procedure for large propositional formulas and with a model checker), and for concurrent and real-time systems (including a transparent embedding of the duration calculus). Collaborative projects involving PVS are ongoing with NASA and several aerospace companies; applications include a microprocessor for aircraft flight-control, diagnosis and scheduling algorithms for fault-tolerant architectures, and requirements specification for the Jet-Select function of the Space Shuttle flight-control system.
PVS is implemented in Common Lisp and runs on most modern workstations (we can probably port it to any Unix machine for which GNU Emacs and a Common Lisp compiler with integrated CLOS are available). A version in Allegro Lisp for Sun SPARCstations is available by anonymous FTP. All PVS installations must be licensed by SRI International, but there is no charge. (We do charge for tapes and for nonstandard versions). The system is fully documented in three volumes (language, system, and prover), and a tutorial is also available.
To obtain a copy of PVS by anonymous FTP, retrieve the files README and INSTALL from directory /pub/pvs on ftp.csl.sri.com [192.12.33.94] and follow the instructions. These files can also be reached via via WWW. For further information on PVS, please send a message to pvs-request@csl.sri.com.
Note: The current version of PVS is a beta-release. The documentation is not too well organized, and is incomplete. There are very few introductory examples (look in /pub/pvs/examples for what there are). For this reason, we do not advertise the availability of PVS very widely; most of the active users of PVS have spent at least a few days here at SRI learning to use the system under our guidance. We expect to release a new version of the system in the spring of 1995, with substantial extensions, uptodate documentation (with an index!), and several introductory examples.
(Information adapted from an on-line overview.)
Over the past several years, a toolkit for LOTOS has been under development at the University of Ottawa. The interpreter is called ELUDO (Environnement LOTOS de l'Universite d'Ottawa), and XELUDO in its X window version.
The main currently operational tools in ELUDO are ISLA, SELA, and GOAL. LMC and LOTEST are also functional, however their user interface is not integrated, thus it is somewhat more difficult to use them.
Thomas A. Henzinger,
Pei-Hsin Ho,
Howard Wong-Toi
Computer Science Department,
Cornell University
(tah|ho|howard)@cs.cornell.edu
We will demonstrate HyTech, the Cornell Hybrid Technology Tool, on the verification and analysis of several hybrid-system benchmarks.
Hybrid systems are computing systems that react, in real time, to both discrete and continuous activities (such as analog signals, real time, and real speed). Typical examples of hybrid systems are embedded systems. Due to the rapid development of digital processor technology, hybrid systems directly control much of what we depend on in our daily lives. Many hybrid systems, ranging from automobiles to aircraft, operate in safety-critical situations, and therefore call for rigorous analysis techniques. Model checking is an algorithmic technique for analyzing finite-state systems that has recently been extended to certain infinite-state systems, including linear hybrid systems [AHH93].
HyTech (The Cornell Hybrid Technology Tool) is a symbolic model checker for linear hybrid systems. We represent hybrid systems as "hybrid automata", an extension of finite-state machines with continuous variables whose dynamics are governed by differential equations. We write requirement specifications in "integrator computation tree logic" (Ictl), a branching-time temporal logic with clock variables for specifying timing constraints. Given a hybrid automaton describing a system and an Ictl formula describing a requirement, HyTech computes the set of system states that satisfy the requirement.
The current version of HyTech consists of a Mathematica main program, and a set of C++ subroutines that make use of Halbwachs' polyhedron manipulation library [HRP94]. We are also re-implementing HyTech entirely in C++. We have applied HyTech to verify more than 30 hybrid-system benchmarks, including a Philips audio control protocol.
The system requirement for this tool is a Sun SPARC workstation.
Amphion is a system that guides a user in developing a diagrammatic formal specification of a problem and then automatically synthesizes a program to solve the problem from this specification. The program consisting of calls to components from a component library, e.g. subroutines from a subroutine library. Amphion is a generic architecture that is specialized to a particular domain and subroutine library through a domain theory and domain-specific theorem-proving tactics. Program synthesis is based upon deductive synthesis (theorem proving); therefore, the synthesized program correctly implements the specification if the domain theory is correct. The demo will show Amphion/NAIF, the application of Amphion to the domain of solar system kinematics as supported by a subroutine library called SPICELIB. SPICELIB was developed at JPL to support the planetary science community in planning and analyzing the observation geometries of solar system bodies in interplanetary scientific missions. A typical example of the kinds of problems that can be solved using Amphion/NAIF is predicting the location of the shadows of the moons of Jupiter on Jupiter's surface as seen by the Galileo spacecraft. The Amphion/NAIF domain theory has been extended to include the theory of a graphics display library also developed at JPL, so that Amphion can generate programs that display wireframe animations of astronomical situations.
The information in this page was prepared by
Jonathan Bowen
J.P.Bowen@reading.ac.uk and
Lynn Marshall
lynnmar@bnr.ca.
It was last substantiatially updated on
18 April 1995, and as such may now be out of date.
This page was provided remotely for
WIFT'95
as part of
the OUCL
archive.