"To Store or Not To Store" Reloaded: Reclaiming Memory on Demand .
FMICS 2006, August 25 -  27, 2006. Bonn (Germany).
Michael Weber and Moritz Hammer.

Model checking of industrial-scale models is usually restricted by memory size. The research addressing this issue can be divided into two groups: Automatically making models smaller by abstraction, and getting more out of the memory available. While the former direction has seen signicant improvements with the advent of CEGAR model checking [3], large-scale model checking still remains an important area of research. In explicit-state model checking, memory size is mostly restricted by the hash table used to detect state revisits. Among the many solutions to this problem, disk-based model checking and lossy hash tables have been proposed. Disk-based model checking basically tries to get a bigger hash table by swapping states to disk. As disk space is much cheaper than RAM, larger state spaces can be checked on normal systems. Disk storage is of course much slower, especially in random-access mode, which establishes the need for adapted algorithms. Lossy hashing makes use of the observation that the hash table is used for avoiding revisits of parts of the state space that have been visited before. While revisiting is costly with respect to runtime, it does not void the correctness of the search result, as long as the hash table is sufcient to ensure termination. Therefore, it can be attempted to remove states from the lossy hash table in order to reclaim their memory and make room for further, hopefully newly discovered states. Behrmann et al. [1] claim that only 10% of the state space needs to be stored, allowing for much larger search spaces; however this will lead to extensive revisits in our experience. Both directions have been given much research, but they have not yet been combined. Disk-based model checking usually does not make attempts to check a model in RAM only, should it turn out to be small enough. Lossy hashing, on the other hand, does not attempt to avoid revisits. By combining both strategies, we obtain an algorithm that avoids extensive revisits by doing disk lookups, but runs in RAM only as long as this is sufcient. This leads to a smoothly degrading algorithm, which adaptively changes its use of memory: For smaller models, it is little different from a RAM-only model checker, and it gradually becomes a disk-based model checker if memory becomes scarce.

GPSL: A Programming Language for Service Implementation.
ETAPS 2006, March 25 -  April 2, 2006. Vienna (Austria).
Dominic Cooney, Marlon Dumas, and Paul Roe.

At present, there is a dichotomy of approaches to supporting web service implementation: extending mainstream programming languages with libraries and metadata notations vs. designing new languages. While the former approach has proven suitable for interconnecting services on a simple point-to-point fashion, it turns to be unsuitable for coding concurrent, multi-party, and interrelated interactions requiring extensive XML manipulation. As a result, various web service programming languages have been proposed, most notably (WS-)BPEL. However, these languages still do not meet the needs of highly concurrent and dynamic interactions due to their bias towards statically-bounded concurrency. In this paper we introduce a new web service programming language with a set of features designed to address this gap. We describe the implementations in this language of non-trivial scenarios of service interaction and contrast them to the corresponding BPEL implementations. We also define a formal semantics for the language by translation to the join calculus. A compiler for the language has been implemented based on this semantics.

Observational Purity and Encapsulation.
ETAPS 2005, April 2 - 10, 2005. Edinburgh (Scotland).
David A. Naumann.

Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be strongly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes and extends a recently proposed notion of observational purity, reducing the proof obligation to a familiar one for equivalence of two class implementations.

Checking Absence of Illicit Applet Interactions: A Case Study.
ETAPS 2004, March 27 - April 4, 2004. Barcelona (Spain).
Marieke Huisman, Dilian Gurov, Christoph Sprenger and Gennady Chugunov.

We present the use of a method – and its corresponding tool set – for compositional
verification of applet interactions on an industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co–existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional,
thus supporting post–issuance loading of applets.

Spatial Security Policies for Mobile Agents in a Sentient Computing Environment.
ETAPS 2003, April 5 - 13, 2003. Warsaw (Poland).
David Scott, Alastair Beresford and Alan Mycroft.

A Sentient Computing environment is one in which the system is able to perceive the state of the physical world and use this information to customise its behaviour. Mobile agents are a promising new programming methodology for building distributed applications with many advantages over traditional client-server designs. We believe that properly controlled mobile agents provide a good foundation on which to build Sentient applications.

The aims of this work are threefold: (i) to provide a simple location-based mechanism for the creation of security policies to control mobile agents; (ii) to simplify the task of producing applications for a pervasive computing environment through the constrained use of mobile agents; and (iii) to demonstrate the applicability of recent theoretical work using ambients to model mobility.

Synthesizing Monitors for Safety Properties.
ETAPS 2002, April 6 - 14, 2002. Grenoble (France).
K. Havelund and G. Rosu.

The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.

Compositional Message Sequence Diagrams.
ETAPS 2001, April 2 - 6, 2001. Genova (Italy).
E. Gunter, Am Muscholl and D. Peled.

Message sequence charts (MSCs) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy both a visual and a textual representation. High level MSCs (HMSCs) allow specifying infinite scenarios and different choices. Specifically, an HMSC consists of a graph, where each node is a finite MSC with matched send and receive events, and vice versa. In this paper we demonstrate a weakness of HMSCs, which disallows one to model certain interactions. We will show, by means of an example, that some simple finite state and simple communication protocol cannot be represented using HMSCs. We then propose an extension to the MSC standard, which allows HMSC nodes to include unmatched messages. The corresponding graph notation will be called HCMSC, which stands for High level Compositional Message Sequence Charts. With the extended framework, we provide an algorithm for automatically constructing an MSC representation for finite state asynchronous message passing protocols.

Molecular Analysis of Metabolic Pathway with Graph Transformation.
ICGT 2006, September 17 - September 23, 2006. Natal, Rio Grande do Norte (Brazil).
K. Ehrig, R. Heckel, and G. Lajios.

Metabolic pathway analysis is one of the tools used in biology and medicine in order to understand reaction cycles in living cells. A shortcoming of the approach, however, is that reactions are analysed only at a level corresponding to what is known as the ’collective token view’ in Petri nets, i.e., summarising the number of atoms of certain types in a compound, but not keeping track of their identity.
In this paper we propose a refinement of pathway analysis based on hypergraph grammars, modelling reactions at a molecular level. We consider as an example the citric acid cycle, a classical, but non-trivial reaction for energy utilisation in living cells. Our approach allows the molecular analysis of the cycle, tracing the flow of individual carbon atoms based on a simulation using the graph transformation tool AGG.

Rule Execution in Graph-Based Incremental Interactive Integration Tools.
ICGT 2004, September 28 - October 2, 2004. Roma (Italy).
S.M. Becker, S. Lohmann, and B. Westfechtel.

Development processes in engineering disciplines are inherently complex. Throughout the development process, different kinds of inter-dependent design documents are created which have to be kept consistent with each other. Graph transformations are well suited for modeling the operations provided for maintaining inter-document consistency. In this paper, we describe a novel approach to rule execution for graph-based integration tools operating interactively and incrementally. Rather than executing a rule in atomic way, we break rule execution up into multiple phases. In this way, the user of an integration tool may be informed about all potential rule applications and their mutual conflicts so that he may take a judicious decision how to proceed.

Transforming Specification Architectures by GenGED.
ICGT 2002, October 7 - 12, 2002. Barcelona (Spain).
Bardohl, R., Ermel, C. and Padberg, J.

This contribution concerns transformations of specification architectures which are diagrams of sub-specifications.
The graph of a diagram presents the architecture: the nodes correspond to the sub-specifications and the edges to specification morphisms. We do not fix a specific visual specification technique, so this approach is in the tradition of high-level replacement systems. We discuss how to transform such specification architectures and    distinguish local and global changes.
The main emphasis of this contribution is the specification and transformation of specification architectures using \GenGEDp.
In GenGED, a visual language (VL) is defined by a visual alphabet and a visual syntax grammar. We define a VL for specification architectures by composing VLs for graphs and for P/T nets enhanced by Petri net morphisms. From this VL definition a syntax-directed editor is generated supporting the editing of consistent specification architectures. Local and global changes of a specific specification architecture then can easily be defined as transformation rules in our VL and visualized in the GenGED environment.

Proof engines for bounded model checking of hybrid systems.
FMICS 2004, September 20 - 21, 2004. Linz (Austria)
Martin Fränzle, and Christian Herde.

In this paper we present HySat, a new bounded model term checker for linear hybrid systems, incorporating a tight integration of a DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.

Distributed State Space Minimization.
FMICS 2003, June 5 - 7, 2003. Trondheim (Norway).
Stefan Blom and Simona Orzan.

It is a known problem that state spaces can grow very big, which makes operating with them (including reducing them) difficult because of memory shortage. In the attempt to extend the size of the state spaces that can be dealt with, we designed and implemented a bisimulation reduction algorithm for distributed memory settings using message passing communication. By using message passing, the same implementation can be used on both large SMP machines and clusters of workstations. The algorithm performs reduction of large labeled transition systems modulo strong bisimulation. We justify its correctness and termination. We provide an evaluation of the worst-case time and message complexity and some performance data from a prototype implementation. Both theory and practice show that the algorithm scales up with the number of workers.

Validating OCL Specifications with the USE Tool—An Example Based on the BART Case Study.
FMICS 2003, June 5 - 7, 2003. Trondheim (Norway).
Paul Ziemann and Martin Gogolla.

The Object Constraint Language (OCL) is part of the Unified Modeling Language (UML). Within software engineering, UML is regarded today as an important step towards development of high-quality object-oriented systems. OCL allows to sharpen UML diagrams through invariants as well as pre- and postconditions. This paper explains the functionality of the UML Specification Environment USE which allows to validate UML and OCL descriptions.
The paper shows that central safety properties of the train system described in the well-known BART case study can be expressed with OCL. Test cases embodying central aspects of this train system can be formulated within the USE system. It can be shown that the safety properties are satisfied by the test cases examined.

Specification of Network Embedded Software Components.
IDPT 2002, June 23 - 28, 2002. Pasadena (California/USA)
Asuman Sünbül.

In the last years, generative component based techniques have already successfully been used within a large number of software development projects. They have shown to be especially useful in applications where certain patterns of system architecture and/or implementation structures can be identified and used as possible starting points for automatically generating system parts from more abstract descriptions. Standard component "developing" techniques being used were CORBA (including real-time CORBA), DCOM or JavaBeans. But there is huge amount of platforms, not necessarily exotic ones, where neither the traditional middleware techniques (e.g CORBA) nor component techniques can be applied. A particular example for those kind of systems, are given by network embedded, real-time, wireless systems. The size of NEST configurations, their tight integration with dynamic, non-stationary physical processes and limitations in component reliability make the use of self-assembly, self-configuration, self-repair and other forms of adaptation mandatory. These requirements push the demand for new tools and methodologies for designing communication protocols and services for distributed systems supporting a third generation of ultra-high performance middleware and light-weighted components. We're presenting our framework for developing light-weighted, formally correct software which is well suiting for the needs of NEST demands.