PVS, ICS and SAL: An Introduction to the State of the Art in Mechanized Formal Methods
For FME 2002, we offer a full-day tutorial on modern formal methods, structured in two halves. The morning will present an overview of PVS suitable for those with no prior experience of the system, followed by a description and demonstration of new capabilities that will be of interest to current users.
The afternoon will introduce two new systems that complement PVS. ICS is a standalone implementation of the decision procedures from PVS that can be used to add powerful automated deductive capabilities to other software. SAL is an environment for analysis of systems specified as state machines; it serves as a tool bus that integrates existing tools such as PVS and off-the-shelf model checkers and static analyzers, and it also provides a scriptable interface that can be used to provide customized tools for abstraction and state exploration.
The tutorials will combine lectures with demonstrations of the actual systems and will focus on their use rather than underlying theory. The intended audience includes those considering using mechanized formal methods for the first time, as well as existing users of PVS and other tools.
In addition to those who will use ICS and SAL directly, the afternoon sessions are also intended for tool developers who will learn how to integrate these systems with their own. Much of the material presented should also interest those attending other FLOC conferences besides FME. Participants in the tutorial will gain insight into the different purposes and markets served by PVS, ICS, and SAL, an appreciation of their capabilities, and the basic knowledge required to start using them.
SRI International freely licenses PVS, ICS, and SAL for academic research purposes. The systems are also available for commercial use. See, for example, this press release by TransEDA. Contact John Rushby to discuss commercial licensing terms.
This session will present an introduction to the basic capabilities of PVS, mainly through an extended demonstration. Information about PVS is available at http://pvs.csl.sri.com/.
Today's tutorial will focus on the capabilities of ICS and how to use them. ICS is implemented in OCaml and can be invoked from other programs as an OCaml module, a Common Lisp interface, or a C library. There is also a simple ascii interface for testing and experiments. And because ICS is used in PVS, it is also possible to experiment in the full PVS system before creating a specialized environment based on ICS. Unlike other standalone decision procedures, ICS has a rich API not only allows it to accept formulas and decide their validity, but that also allows querying and canonization against a database of formulas that can be asserted and retracted in near-constant time. This allows it to be used in proof search rather than simply to discharge individual leaves of a proof.
ICS can be used as the core of applications that need powerful deductive capabilities, such as checkers for tabular specifications, test-case generators, and others still to be invented. We envisage that it will be used to embed formal methods "invisibly" within traditional engineering development tools. As one example, use of ICS in combination with an efficient SAT solver to provide bounded model checking for infinite domains will be described in a paper presented at CADE
SAL functions as a tool bus and as a repository for specifications and analyses. Specifications are written in the SAL language, which is a very general language for describing state machines. SAL provides modules, guarded assignments, and both synchronous and asynchronous composition. SAL is defined as an XML DTD, but we also provide a prettyprinter and parser to and from a textual format. It is straightforward to write translators between SAL and most other state machine languages: we provide translators from Stateflow and from Lustre to SAL, and from SAL to SMV, as examples.
SAL specifications can be defined over various built-in types (such as integers and subranges), or over types defined in PVS. There is no requirement for SAL specifications to be finite state. Infinite-state specifications can be analyzed by PVS, or they can be reduced to finite-state, or other special form, using predicate and data abstraction. Such abstracted specifications can then be translated to the form accepted by a specialized tool such as a model checker. The tool may decide some property of the abstracted specification (e.g., whether it satisfies a specification expressed as a CTL formula), or it may return information about the specification (e.g., a counterexample, or the set of reachable states expressed as a BDD). The new information may assist construction of an improved abstraction, and the analysis may proceed through several steps of abstraction, analysis, and refinement, involving several tools. SAL keeps track of the abstractions and analyses performed, and of the status of properties that are to be verified.
Although SAL can employ front-end languages and back-end tools from external providers, it is also equipped with a powerful and flexible environment of its own for statespace exploration. This environment, SALENV, provides an API for efficient manipulation and exploration of explicit and symbolic states and for the construction of B\"{u}chi automata; simple scripts written in the Scheme programming language then yield efficient LTL model checkers that can be modified to use a variety of exploration strategies (e.g., depth-first, or iterative deepening) and optimizations (e.g., partial order or symmetry reductions). Other simple scripts can construct visualizations of a state space, or calculate properties such as maximum blocking time for a real-time scheduler.
This session will outline the new "workflow" for formal analysis supported by SAL, and will provide an introduction to the SAL language and the SALENV environment.
Go to the SRI Formal Methods page (you can find our
papers here by searching or following links to people's home pages).
John Rushby (Rushby@csl.sri.com)