Formal Techniques for Networked and Distributed Systems – FORTE 2004

As its name indicates, NGSCB aims to be the ”Next-Generation Secure Computing Base”. As envisioned in the context of Trusted Computing initiatives, NGSCB provides protection against software attacks. This paper describes NGSCB using a logic for authentication and access control. Its goal is to document and explain the principals and primary APIs employed in NGSCB.

Event-based process algebraic specification languages support an elegant specification technique by which system behaviours are described as compositions of constraints on event occurrences and event parameters. This paper investigates the possibility to export this specification paradigm to a state-based formalism, and discusses some deriving advantages in terms of verification.

Software engineering is based today to a large extend on rapid prototyping languages or design environments which are high level, very expresive, executable and enabling the quick production of running prototypes, whereas formal methods emphasices the preciseness and proper mathematical foundations which eanble the production of unambiguous references needed in protocol engineering. The goals of formal methods and rapid prototyping are not in contradiction, but have very rarely been considered together. This paper analyzes the evolution, background and main divergence points, in order to highligh how convergence could be achieved.

Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioural semantics of ProActive objects. Our models are symbolic networks of labelled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software tool set for the analysis of ProActive applications using these methods.

UML and SDL are languages for the development of software systems that have different origins, and have evolved separately for many years. Recently, it can be observed that OMG and ITU, the standardisation bodies responsible for UML and SDL, respectively, are making efforts to harmonise these languages. So far, harmonisation takes place mainly on a conceptual level, by extending and aligning the set of language concepts. In this paper, we argue that harmonisation of languages can be approached both from a syntactic and semantic perspective. We show how a common basis can be derived from the analysis of the UML meta-model and the SDL abstract grammar. For this purpose, conceptually sound and well-founded mappings from meta-models to abstract grammars and vice versa are defined and applied. The long term objective is the syntactic and semantic integration of UML and SDL. The key to achieving this objective is a common language core, which can then be extended in different ways to cover further, more specific language concepts, and is sufficiently flexible to support future language add-ins.

We present automated techniques for the explanation of counter-examples, where a counter-example should be understood as a sequence of program statements. Our approach is based on variable dependency analysis and is applicable to programs written in Cimple, an expressive subset of the C programming language. Central to our approach is the derivation of a focus-statement sequence (FSS) from a given counter-example: a subsequence of the counter-example containing only those program statements that directly or indirectly affect the variable valuation leading to the program error behind the counter-example. We develop a ranking procedure for FSSs where FSSs of higher rank are conceptually easier to understand and correct than those of lower rank. We also analyze constraints over uninitialized variables in order to localize program errors to specific program segments; this often allows the user to subsequently take appropriate debugging measures. We have implemented our techniques in the FocusCheck model checker, which efficiently checks for assertion violations in Cimple programs on a per-procedure basis. The practical utility of our approach is illustrated by its successful application to a fast, linear-time median identification algorithm commonly used in statistical analysis and in the Resolution Advisory module of the Traffic Collision Avoidance System.

We describe a semi-automated verification of a slightly optimised version of Michael and Scott’s lock-free FIFO queue implementation. We verify the algorithm with a simulation proof consisting of two stages: a forward simulation from an automaton modelling the algorithm to an intermediate automaton, and a backward simulation from the intermediate automaton to an automaton that models the behaviour of a FIFO queue. These automata are encoded in the input language of the PVS proof system, and the properties needed to show that the algorithm implements the specification are proved using PVS’s theorem prover.

In this paper, we present an approach for modeling an existing web application using communicating finite automata model based on the user-defined properties to be validated. We elaborate a method for automatic generation of such a model from a recorded browsing session. The obtained model could then be used to verify properties with a model checker, as well as for regression testing and documentation. Unlike previous attempts, our approach is oriented towards complex multi-window/frame applications. We present an implementation of the approach that uses the model checker Spin and provide an example.

This paper proposes an algorithm for the construction of an MSC graph from a given set of actual behaviors of an existing concurrent system which has repetitive subfunctions. Such a graph can then be checked for safe realizability and be used as input to existing synthesis techniques.

Passive testing has proved to be a powerful technique for protocol system fault detection by observing its input/output behaviors yet without interrupting its normal operations. To improve the fault detection capabilities we propose a backward checking method that analyzes in a backward fashion the input/output trace from passive testing and its past. It effectively checks both the control and data portion of a protocol system, compliments the forward checking approaches, and detects more errors. We present our algorithm, study its termination and complexity, and report experiment results on the protocol SCP.

We show that the test generation task can be carried out by solving a reachability problem in a system consisting essentially of a specification of the communicating system and its fault model. Our technique can be applied using most off-the-shelf model-checking tools to synthesize minimal test sequences, and we demonstrate it using the UppAal real-time model-checker.

We present two algorithms for generating minimal tests: one for single faults and one for multiple faults. Moreover, we demonstrate how to exploit the unique time- and cost-planning- facilities of UppAal to derive cheapest possible test suites for restricted types of timed systems.

In this paper we use equation solving for translating internal tests derived for a component embedded within a composite system into external tests defined over the external alphabets of the system. The composite system is represented as two communicating finite state machines (FSMs), an embedded component FSM, and a context FSM that models the remaining part of the system and which is assumed to be correctly implemented. Application example is given to demonstrate the steps of the method. The method can be adapted for test derivation for a system of two or more communicating FSMs.

Distributed real-time systems are of one important type of real-time systems. They are usually characterized by both reactive and real-time factors and it has long been recognized that how to automatically check such systems’ correctness at run time is still an unaddressed problem. As one of the main solutions, test oracle is a method usually used to check whether the system under test has behaved correctly on a particular execution. Test oracle is not only the indispensable stage of software testing, but also the weak link of the software testing research. In this paper, real-time specifications are adopted to describe the properties of distributed real-time systems and a real-time specification-based method for automatic run-time test oracles generating is proposed. The method proposed here is based on tableau construction theory of real-time model checking, automatically generates timed automata as test oracles, which can automatically check system behaviors’ correctness from real-time specifications written in MITL_[0,d].

Eliciting, modeling, and analyzing the requirements are the main challenges to face up when you want to produce a formal specification for distributed systems. The distribution and the race conditions between events make it difficult to include all the possible scenario combinations and thus to get a complete specification. Most research about formal methods dealt with languages and neglected the process of how getting a formal specification. This paper describes a scenario-based process to synthesize a formal specification in the case of a distributed system. The requirements are represented by a set of use cases where each one is composed of a collection of distributed scenarios. The architectural assumptions about the communication between the objects of the distributed system imply some completions and reorganizations in the use cases. Then, the latter are composed into a global finite state machine (FSM) from which we derive a communicating FSM per object in the distributed system.

Controllability and observability problems may manifest themselves during the application of a test or checking sequence in a test architecture where there are multiple remote testers. These problems often require the use of external coordination message exchanges among testers during testing. It is desired to construct a test or checking sequence from the specification of the system under test such that it will be free from these problems without requiring the use of external coordination messages. This paper investigates conditions that allow us to construct such a test or checking sequence. For specifications satisfying these conditions, procedures for constructing subsequences that eliminate the need for using external coordination messages are given.

Witnesses and counterexamples produced by model checkers provide a very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specified with a CCS-like process algebra. There, only linear and finite witnesses and counterexamples are useful and for the given formula and model an efficient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identifies a fragment of action computation tree logic (ACTL) that can be handled in this way. Moreover, a suitable form of witnesses and counterexamples is proposed and witness and counterexample automata are introduced, which are finite automata recognizing them. An algorithm for generating such automata is given.

Symmetry based approaches are known to attack the state space explosion problem encountered during the analysis of distributed systems. In another way, BDD-like encodings enable the management of huge data sets. In this paper, we show how to benefit from both approaches automatically. Hence, a quotient set is built from a coloured Petri net description modeling the system. The reachability set is managed under some explicit symbolic operations. Also, data representations are managed symbolically based on a recently introduced data structure, called Data Decisions Diagrams, that allow flexible definition of application specific operators. Performances yielded by our prototype are reported in the paper.

The main goal of this paper is to extend sPBC with the iteration operator, providing an operational semantics for the language, as well as a denotational semantics, which is based on stochastic Petri nets. With this new operator we can model some repetitive behaviours, and then we obtain a formal method that can be easily used for the design of communication protocols and distributed systems.

In this paper we propose a translation into high level Petri nets of a finite fragment of the π-calculus. Our construction renders in a compositional way the control flow aspects present in π-calculus process expressions, by adapting the existing graph-theoretic net composition operators. Those aspects which are related to term rewriting, as well as name binding, are handled through special inscription of places, transitions and arcs, together with a suitable choice of the initial marking for a compositionally derived high level Petri net.

Monitoring large distributed concurrent systems is a challenging task. In this paper we formulate (model-based) diagnosis by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach: the model defines explicitly the causal and concurrency relations between the observable events, produced by the system under supervision on different points of observation. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. In this paper we extend our first method based on Petri nets unfolding to high-level parameterized Petri nets. This allows the designer to model data aspects (even on infinite domains) and non deterministic actions. The observation of such an action gives only partial information and the supervisor has to introduce parameters to represent the hidden aspects of the reached state. This supposes that the possible values for the parameters are symbolically computed and refined during supervision. In practice, non deterministic actions can also be used as an approximation to deal with incomplete information about the system. In this case the refinement of the parameters during supervision improves the knowledge of the model.

Numerous specialized ad hoc routing protocols are currently proposed for use, or being implemented. Few of them have been subjected to formal verification. This paper evaluates two model checking tools, SPIN and UPPAAL, using the verification of the Lightweight Underlay Network Ad hoc Routing protocol (LUNAR) as a case study. Insights are reported in terms of identifying important modeling considerations and the types of ad hoc protocol properties that can realistically be verified.

We propose a framework for intrusion detection that is based on runtime monitoring of temporal logic specifications. We specify intrusion patterns as formulas in an expressively rich and efficiently monitorable logic called Eagle. Eagle supports data-values and parameterized recursive equations, and allows us to succinctly express security attacks with complex temporal event patterns, as well as attacks whose signatures are inherently statistical in nature. We use an online monitoring algorithm that matches specifications of the absence of an attack, with system execution traces, and raises an alarm whenever the specification is violated. We present our implementation of this approach in a prototype tool, called Monid and report our results obtained by applying it to detect a variety of security attacks in log-files provided by DARPA.

Erratum to: D. de Frutos-Escrig and M. Núñez (Eds.) Formal Techniques for Networked and Distributed Systems -- FORTE 2004 DOI: 10.​1007/​978-3-540-30232-2

The book was inadvertently published with an incorrect name of the copyright holder. The name of the copyright holder for this book is: © IFIP International Federation for Information Processing. The book has been updated with the changes.