__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 faultrecovering 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 faulttolerance 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 byproduct 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