Provably Correct Code Generation: A Case Study 

Authors:  Qian Wang, Gopal Gupta (Univ. of Texas at Dallas, USA)

Abstract. Provably correct compilation is an important aspect in development of high assurance
software systems. In this paper we present an approach to provably correct compilation based on Horn
logical semantics of programming languages and partial evaluation. We also show that continuation
semantics can be expressed in the Horn logical framework, and introduce Definite Clause Semantics.
We illustrate our approach by developing a complete semantics for the SCR specification language, and
using it to (automatically) generate target code in a provably correct manner.
 

  A Denotational Approach to the Static Analysis of Cryptographic Processes

Authors: Benjamin Aziz, G.W. Hamilton and D. Gray (Dublin City University, Ireland)
Abstract:
We present in this paper, a non-uniform static analysis for detecting the term-substitution property in
processes specified in the spi calculus. The property is essential in defining security breaches, like
secrecy and authenticity. The analysis is fully denotational, preserving compositionality and facilitating
implementations in functional programming.

  Verification of Scenario-based Specifications using Templates 

Authors: Girish Palshikar, Purandar Bhaduri (Tata Research Development and Design Centre, India)

Abstract: Specifying dynamic behaviour of a system by listing scenarios of its
interactions has become a popular practice. Message sequence chart (MSC) is a
rigorous and widely used notation for specifying such scenarios of system behaviour.
High-level MSCs (HMSC) provide hierarchical and modular composition
facilities for constructing complex scenarios from basic MSCs. Although
the general problem of formal verification of properties of HMSCs is intractable,
we propose a framework for restricted verification. We present simple templates
for commonly useful types of properties and discuss efficient algorithms
for verifying them.

   A Trace Logic for Local Security Properties  

Authors:  Ricardo Corin, Antonio Durante, Sandro Etalle, Pieter Hartel  (Univ. of Twente, Netherlands and Universita di Roma, Italy)

Abstract: We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specification. Our technique allows a protocol designer to provide formal specification of the desired security properties, and integrate them naturally into the design process of cryptographic protocols. Furthermore, the logic can be used for formal verification. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.

 Logical Specification and Analysis of Fault Tolerant Systems Through Partial Model Checking 

Authors: S. Gnesi, G. Lenzini and F. Martinelli  (C.N.R., Italy)

Abstract. This paper presents a logical characterization of fault tol­
erance and proposes a framework for a formal analysis based on partial
model checking techniques. Our framework requires a fault tolerant (can­
didate) systems to be modeled using a formal calculus, for example the
CCS process algebra. To this aim we propose a uniform modeling scheme
in which to specify a formal model of the system, its failing behavior (with
respect to fault occurrences) and possibly its fault­recovering procedures.
Once a formal model is provided into our scheme, fault tolerance with
respect to a given property, can be formalized, in a logic formalism, as an
equational µ­calculus formula expressing all the fault scenarios satisfying
that property. This logical characterization understands the analysis of
fault tolerance as a form of analysis of open systems. Thank to partial
model checking strategies such a characterization can be made indepen­
dent on any particular fault assumption. Such a logic characterization
makes possible the fault­tolerance verification problem be expressed as a
general µ­calculus validation problem, for solving which many theorem
proof techniques and tools are available. Moreover we present several
analysis methods that show how much flexible is our approach.
Keywords: Fault Tolerant Systems, Formal Verification, Partial Model Checking

 Compositional Properties of Sequential Processes 

Authors: Naijun Zhan (Mannheim Universitat, Germany)

Abstract. It is widely agreed that the modular method is one of the
most effective methods to specify and verify complex systems in order to
avoid combinatorial explosion. FLC ( Fixpoint Logic with Chop) is an
important modal logic because of its expressivity and logic properties,
e.g., it is strictly more expressive than the µ­calculus. In this paper, we
study the compositionality of FLC, namely, to investigate the connection
between the connectives of the logic and the constructors of programs.
To this end, we firstly extend FLC with a nondeterministic operator ``+''
(FLC + for the extension) and then establish a correspondence between
the logic and the basic process algebra with deadlock and termination
(abbreviated by BPA # # ). Finally, we show that as a by­product of the
correspondence characteristic formulae for strong ( observational) bisim­
ulation on BPA # # can be constructed compositionally directly from the
syntax of processes.
Keywords: chop operator, modal logic, compositionality, verification, bisim­
ulation, characteristic formula, process algebra

 Equational Abstractions for Model Checking Erlang Programs

Authors: Thomas Noll (Aachen University, Germany)

Abstract
This paper provides a contribution to the formal verification of programs written in the con­
current functional programming language Erlang, which is designed for telecommunication appli­
cations. It presents a formal description of this language in Rewriting Logic, a unified semantic
framework for concurrency which is semantically founded on conditional term rewriting modulo
equational theories. In particular it demonstrates the use of equations for defining abstraction
mappings which reduce the state space of the system.

 Verifying a UMTS protocol using SPIN and EASN 

Authors: M. Luukkainen, Vivek K. Shanbhag and K. Gopinath (University of Helsinki, Finland and  Indian Institute of Science)

Abstract:  Next generation mobile protocols have become very complex and it is becoming increasingly difficult for standards bodies to be sure of the correctness of protocols during the standardization process. A convenient notation for specifying protocols and a means to analyze their behavior at a certain level of abstraction could be quite useful. Model-checking has turned out to be an efficient and relatively easy-to-use technique in the verification of formally described behaviors. However, there are two major drawbacks in using model-checking: one is state explosion (the behavior models of real-life programs tend to be extremely large); the other factor limiting industrial applicability of model checkers is their restricted input language. For instance, in the field of telecommunications, the standards define the data model of the protocols using the ASN.1 notation and it would be simpler if the verification models could be directly built using this 'native' data definition language of the telecommunication industry.

In this paper, we consider model checking in the RLC protocol in the UMTS system that is seeing ongoing development as a third generation mobile communication system. We briefly describe EASN, a model checker wherein the behavior can be formally specified through a language based upon Promela for control structures but with data models form ASN.1 We discuss the verification problem for RLC and then discuss the results of using EASN on the verification problem and compare with SPIN which is also the basis for the EASN realization.

As a side-effect of realizing EASN, we have been able to locate some intricate performance bugs in the SPIN implementation. We believe that this type of "n-version" programming is necessary to increase confidence in model checkers.

Keywords: Model Checking, Spin, Promela, ASN.1, Telecommunication protocols, RLC, UMTS

 Insights to Angluin's Learning   

Authors:  Therese Berg, Bengt Jonsson, Martin Leucker, Mayank Saksena (Uppsala Univ, Sweden)

Abstract
Among other domains, learning finite-state machines is important for obtaining a
model of a system under development, so that powerful formal methods such as
model checking can be applied.

A prominent algorithm for learning such devices was developed by Angluin. We
have implemented this algorithm in a straightforward way to gain further insights to
practical applicability. Furthermore, we have analyzed its performance on randomly
generated as well as real-world examples. Our experiments focus on the impact of
the alphabet size and the number of states on the needed number of membership
queries. Additionally, we have implemented and analyzed an optimized version
for learning prefix-closed regular languages. Memory consumption is one major
obstacle when we attempted to learn large examples.
We see that prefix-closed languages are relatively hard to learn compared to
arbitrary regular languages. The optimization, however, shows positive results.
Key words: deterministic finite-state automata, learning
algorithm, regular languages, prefix-closed regular languages