Due to its capabilities to integrate well with C code, Spin has been used for C code verification based on environment models that describe the context, in which the software under verification is expected to run. In practice this approach requires an in-depth knowledge of Promela and the underlying technology. Moreover environment models tend to be verbose and exhibit heavily intertwined statements of Promela and C code. Thereby, writing and understanding such hybrid models is difficult and error-prone. Alleviating this problem we develop a specialized language for expressing environment models used in verification harnesses. Our language harmonizes the use of Promela and C in a homogeneous way that is suitable for practitioners. We show how a small number of language concepts is sufficient to define environments for a wide variety of commonly encountered software components written in C. The approach is integrated in the development platform mbeddr, a technology stack for embedded programming and formal verification developed on top of JetBrains’ MPS language workbench.

The paper summarizes our experiences in applying formal verification using the explicit-state model checker SPIN and combining it with a model-based testing approach to support the validation of embedded software. The discussed example covers a crucial part of the firmware of the fault-tolerant programmable logic controller Siemens SIMATIC S7-400H. The chosen approach is outlined and obstacles that were faced during the project are discussed. The paper advocates why formal verification is not suitable as a standalone method in industrial projects. Rather it must be combined with an appropriate validation method such as testing to maximize the benefits from the combination of both approaches. In this case, formal verification complements code or design model reviews, and testing benefits from the availability of correct formal models provided during verification process.

The wide-scale introduction of model-based testing techniques in an industrial context faces many obstacles. One of the obstacles is the existing methodology gap between informally described test purposes and formally defined test descriptions used as the starting point for test automation. The provision of an explicit test description becomes increasingly essential when integrating complex, distributed systems and providing support for conformance and interoperability tests of such systems. The upcoming ETSI standard on the Test Definition Language (TDL) covers this gap. It allows describing scenarios on a higher abstraction level than programming or scripting languages. Furthermore, TDL can be used as an intermediate representation of tests generated from other sources, e.g. simulators, test case generators, or logs from previous test runs. TDL is based on a meta-modelling approach that expresses its abstract syntax. Deploying this design approach, individual concrete syntaxes of TDL can be designed for different application domains. The paper provides an overview of TDL and discusses its application on a use case from the rail domain.

Abstract A formal framework for the analysis of execution traces collected from distributed systems at run-time is presented. We introduce the notions of event and message traces to capture the consistency of causal dependencies between the elements of a trace. We formulate an approach to property testing where a partially ordered execution trace is modeled by a collection of communicating automata. We prove that the model exactly characterizes the causality relation between the events/messages in the observed trace and discuss the implementation of this approach in SDL, where ObjectGEODE is used to verify properties using model-checking techniques. Finally, we illustrate the approach with industrial case studies.

This summary reports on the one-day Workshop on Testing Distributed Componem-Based Systems (TDCS) that took place in affiliation with the International Conference on Software Engineering (ICSE) in Los Angeles in May 1999. The workshop dealt with new advances m test methods and test technologies for the emerging class of &stributed component-based systems that are built on basis of middleware software like COM, CORBA, or Java RMI, including syslems comprising Commercial-Off-The-Shelf (COTS) components The around thirty workshop attendees discussed what efforts m software technology and research are required to cope with testing such systems. Twelve papers out of nineteen submissions were presented.