Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System.
- Alessandro Cimatti,Fausto Giunchiglia,Giorgio Mongardi,Dario Romano,Fernando Torielli,Paolo Traverso,Ansaldo Segnalamento Ferroviario (asf,Ansaldo Trasporti (atr
This paper reports on an experience in formal verification using spin. The
analyzed system is the Safety Logic of an interlocking system for the control
of railway stations developed by Ansaldo. The Safety Logic is a process-based
software architecture, which can be configured to implement different functions
and control stations of different topology.
In this paper we describe how a promela model has been devised, which
retains the configurability features of this architecture. Furthermore, we discuss
the verification with spin of significant process configurations.
This paper describes a joint project between Ansaldo and IRST. The goal of the project
was the evaluation of the possibility to integrate formal...
The Practice of Logical Frameworks
- Frank Pfenning
Deductive systems, given via axioms and rules of inference, are a common conceptual
tool in mathematical logic and computer science. They are used to specify
many varieties of logics and logical theories as well as aspects of programming
languages such as type systems or operational semantics. A logical framework
is a meta-language for the specification of deductive systems. Research on logical
frameworks is still in its infancy. Nonetheless, different frameworks have
been proposed, implemented, and applied to a variety of problems. In addition,
some general reasoning systems have been used to study deductions as
mathematical objects, without specific support for the domain of deductive systems.
This short survey cannot...
A Logical View Of Concurrent Constraint Programming
- Nax P. Mendler,Prakash Panangaden,P. J. Scott,R. A. G. Seely
. Concurrent Constraint Programming (CCP) has been the subject of
growing interest as the focus of a new paradigm for concurrent computation. Like
logic programming it claims close relations to logic. In fact CCP languages are
logics in a certain sense that we make precise in this paper. In recent work it
was shown that the denotational semantics of determinate concurrent constraint
programming languages forms a fibred categorical structure called a hyperdoctrine,
which is used as the basis of the categorical formulation of first-order logic. What
this shows is that the combinators of determinate CCP can be viewed as logical
connectives. In this paper we extend these ideas...
Natural Deduction for Intuitionistic Non-Commutative Linear Logic
- Jeff Polakow
. We present a system of natural deduction and associated
term calculus for intuitionistic non-commutative linear logic (INCLL) as
a conservative extension of intuitionistic linear logic. We prove subject
reduction and the existence of canonical forms in the implicational fragment.
We also illustrate by means of an example how the proof term
calculus can be employed in the setting of logical frameworks to capture
useful representation invariants.
Intuitionistic logic captures pure functional computation in a logical way, as can
be seen from the Curry-Howard isomorphism between constructive proofs and
functional programs. However, there are many structural properties of programs
that are not captured within the intuitionistic framework, such as...
Termination Analysis for Partial Functions
- Jurgen Brauburger,Jurgen Giesl
. This paper deals with automated termination analysis for
partial functional programs, i.e. for functional programs which do not
terminate for each input. We present a method to determine their domains
(resp. non-trivial subsets of their domains) automatically. More
precisely, for each functional program a termination predicate algorithm
is synthesized, which only returns true for inputs where the program is
terminating. To ease subsequent reasoning about the generated termination
predicates we also present a procedure for their simplification.
Termination of algorithms is a central problem in software development and
formal methods for termination analysis are essential for program verification.
While most work on the automation of termination proofs has...
- Disjunctive Chronolog Gergatsoulis,T. Panayiotopoulos
A disjunctive temporal logic programming language, called Disjunctive Chronolog is presented
in this paper. Disjunctive Chronolog combines the ideas of both temporal logic programming
and disjunctive logic programming. The new language is capable of expressing
dynamic behaviour as well as uncertainty, two notions that are very common in a variety of
real systems. Minimal model semantics, model state semantics and øxpoint semantics are
developed for the proposed language and their equivalence is shown.
Keywords: Temporal logic programming, disjunctive logic programming.
Temporal logic programming[OM94, Org91] has been widely used as a means for describing systems
that are inherently dynamic. For example, consider the following Chronolog[Wad88] program
simulating the operation...
Towards an infinitary logic of domains: Abramsky logic for transition systems
- Marcello M. Bonsangue,Joost N. Kok
We give a new characterization of sober spaces in terms of their completely distributive
lattice of saturated sets. This characterization is used to extend Abramsky's results about
a domain logic for transition systems. The Lindenbaum algebra generated by the Abramsky
finitary logic is a distributive lattice dual to an SFP-domain obtained as a solution of a
recursive domain equation. We prove that the Lindenbaum algebra generated by the infinitary
logic is a completely distributive lattice dual to the same SFP-domain. As a consequence
soundness and completeness of the infinitary logic is obtained for a class of transition systems
that is computational interesting.
Complete partial orders were originally...
Formal Methods and the Certification of Critical Systems
- John Rushby
This report was prepared to supplement a forthcoming chapter on formal methods
in the FAA Digital Systems Validation Handbook
. Its purpose is to outline
the technical basis for formal methods in computer science, to explain the use of
formal methods in the specification and verification of software and hardware requirements,
designs, and implementations, to identify the benefits, weaknesses, and
difficulties in applying these methods to digital systems used in critical applications,
and to suggest factors for consideration when formal methods are offered in support
The report assumes a serious interest in the engineering of critical systems, and
a willingness to read occasional mathematical formulas and specialized terminology,
Performance Prediction for the HTMT: A Programming Example
- Jose Nelson Amaral,Guang R. Gao,Phillip Merkey,Thomas Sterling,Zachary Ruiz,Sean Ryan
This paper presents an analytical performance prediction
for the implementation of Cannon's matrix multiply
algorithm in the Hybrid Technology Multi-Threading
(HTMT) architecture . The HTMT subsystems are
built from new technologies: super-conducting processor
elements (called SPELLs ), a network based on
RSFQ (Rapid Single Flux Quantum) logic devices (called
Dependence Speculative Multithreaded Architecture
- Pedro Marcuello
Boosting instruction level parallelism in dynamically scheduled processors requires a large instruction
window. The approach taken by current superscalar processors to build the instruction window is known to
have important limitations, such as the requirement of more powerful instruction fetch mechanisms and the
increasing complexity and delay of the issue logic. In this paper we present a novel processor architectures
(which is called DeSM) that takes a completely different approach to build a large instruction window. The
idea is to identify at run-time sections of code that correspond to loops and execute concurrently several
iterations even if they are dependent. Unlike superscalar processors, instructions are not...
- William W. Cohen,Haym Hirsh
We present a series of theoretical and experimental
results on the learnability of description
logics. We first extend previous
formal learnability results on simple description
logics to C-Classic, a description logic
expressive enough to be practically useful.
We then experimentally evaluate two extensions
of a learning algorithm suggested
by the formal analysis. The first extension
learns C-Classic descriptions from individuals.
(The formal results assume that examples
are themselves descriptions.) The second
extension learns disjunctions of C-Classic
descriptions from individuals. The experiments,
which were conducted using several
hundred target concepts from a number of
domains, indicate that both extensions reliably
learn complex natural concepts.
One well-known family of formalisms for representing
knowledge are description logics, sometimes also called
First Order Linear Logic Without Modalities is NEXPTIME-Hard
- Patrick Lincoln,Andre Scedrov
The decision problem is studied for the nonmodal or multiplicative-additive
fragment of first order linear logic. This fragment is shown to be nexptime-
hard. The hardness proof combines Shapiro's logic programming simulation
of nondeterministic Turing machines with the standard proof of the pspace-
hardness of quantified boolean formula validity, utilizing some of the surprisingly
powerful and expressive machinery of linear logic.
Linear logic, introduced by Girard, is a resource-sensitive refinement of classical
logic [10, 29]. Linear logic gains its expressive power by restricting the
"structural" proof rules of contraction (copying) and weakening (erasing).
The contraction rule makes it possible to reuse any stated assumption as
often as desired. The...
The Hyperfinite Signal: Application To The Modelling Of Discrete Events Systems Behaviour
- Jean-paul Frachet,Rine Lamperiere,Jean-marc Faure
The notion of hyperfinite signal enables to describe the
temporal evolution of a discrete value in a formalism similar to
the one of continuous values evolving in a continuous time. It
relies on an original model of time and discrete values. A
subtype allows the modelling of discrete events systems.
Grafcet, behaviour, temporal logic, non standard analysis,
1. OBSERVATION OF THE TEMPORAL EVOLUTION
OF A PHENOMENON
The time evolution of physical values can be described,
formally or informally, by a function x = f(t) where x is the
modelling of a value and t is the modelling of the time.
In the natural sciences such as physics or mechanics, a
Equational Inference, Canonical Proofs, And Proof Orderings
- Leo Bachmair,Nachum Dershowitz
We describe the application of proof orderings---a technique for reasoning about inference
systems---to various rewrite-based theorem-proving methods, including refinements of the standard
Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for
rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard
completion); and a proof by consistency procedure for proving inductive theorems.
This is a substantially revised version of the paper, "Orderings for equational proofs," co-authored with J. Hsiang
and presented at the Symp. on Logic in Computer Science (Boston, Massachusetts, June 1986). It includes material
from the paper "Proof by consistency in equational theories," by the first author, presented at the Third...
Specifications with Observable Formulae and Observational Satisfaction Relation
- Teodor Knapik
We consider algebraic specifications with observational features.
Axioms as well as observations are formulae of full (ManySorted)
First Order Logic with Equality. The associated semantics is
based on a non standard interpretation of equality called observational
equality. We study the adequacy of this semantics for software specification
and the relationship with behavioural equivalence of algebras.
We show that this framework defines an institution.
Keywords: algebraic specification, observability, semantics.
Within an observational approach the loose semantics of a specification
may either be defined as a class of algebras observationally equivalent to
models satisfying the specification in the usual sense or as a class of algebras
observationally satisfying the specification. The former...
A Proof Theoretic View of Constraint Programming
- Krzysztof R. Apt
. We provide here a proof theoretic account of constraint programming that attempts
to capture the essential ingredients of this programming style. We exemplify it by
presenting proof rules for linear constraints over interval domains, and illustrate their use
by analyzing the constraint propagation process for the SEND + MORE = MONEY puzzle. We
also show how this approach allows one to build new constraint solvers.
Keywords: constraints, constraint propagation, proof rules, linear constraints.
One of the most interesting recent developments in the area of programming has been constraint
programming. A prominent instance of it is constraint logic programming exemplified by such
programming languages as CLP(R),...
Constraint Oriented Specification for Timed CSP
- Jeremy Bryans
A popular specification style, particularly for the initial specification of a system, is the
constraint-oriented style; for example specifying temporal and behavioural aspects separately.
While this style is appealing, it can be hard to apply in practice, because languages which are
designed to describe easily one type of constraint are not always able to easily capture another
type. In this paper, we develop a framework in which a specification is a pair (P ; OE), where P
is a CSP process and OE is a formula of Propositional Temporal Logic (PTL). CSP (Communicating
Sequential Processes) is a process-algebraic language designed for the specification and
analysis of parallel...
Well-Founded Semantics for Extended Logic Programs with Dynamic Preferences
- Gerhard Brewka,Tu Wien,Abteilung Fur Wissensbasierte Systeme
The paper describes an extension of well-founded semantics for logic programs with
two types of negation. In this extension information about preferences between rules can
be expressed in the logical language and derived dynamically. This is achieved by using
a reserved predicate symbol and a naming technique. Conflicts among rules are resolved
whenever possible on the basis of derived preference information. The well-founded conclusions
of prioritized logic programs can be computed in polynomial time. A legal reasoning
example illustrates the usefulness of the approach.
1. Introduction: Why Dynamic Preferences are Needed
Preferences among defaults play a crucial role in nonmonotonic reasoning. One source of
preferences that has been studied...
Simulation, Theory, and Cut Elimination
- Dr. G. White
This paper is concerned with the contrast between simulation- and
deduction-based approaches to reasoning about physical objects. We
show that linear logic can give a unified account of both simulation
and deduction concerning physical objects; it also allows us to draw a
principled distinction between simulation and deduction, since simulations
correspond to cut-free proofs, whereas deductions correspond
to proofs in general.
During the preparation of this work, the author was paid by Project Dynamo, supported
by the United Kingdom Engineering and Physical Sciences Research Council under
grant number GR/K 19266. The views expressed in this paper are the author's own, and
the principal investigators of the project -- John Bell...
Autonomous Navigation using an Adaptive Hierarchy of Multiple Fuzzy-Behaviors
- Edward Tunstel,H. Danny,M. Jamshidi
Adaptive behavioral capabilities are necessary for
robust mobile robot navigation in non-engineered environments.
Robust behavior requires that uncertainty
be accommodated in the robot control system, especially
when autonomy is desired. Fuzzy logic control
technology enables development of controllers which
can provide the necessary computational intelligence
in real-time. This paper presents the incorporation
of fuzzy logic, into the framework of behavior-based
control. An architecture for hierarchical behavior control
is presented in which control decisions result from
a consensus of behavioral recommendations. Multiple
fuzzy-behavior coordination is discussed and applied to
autonomous navigation without explicit maps. Performance
and robustness is demonstrated by implementation
on a mobile robot with significant mechanical
Motion control solutions for mobile robotics are