Search

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.

Formal verification is not always applicable to large industrial software systems due to scalability issues and difficulties in formal model and requirements specification. The scalability and model derivation problems could be alleviated by runtime trace analysis, which combines both testing and formal verification. We implement and compare an ad-hoc custom approach and a formal approach to detect common bug patterns in multithreaded Java software. We use the tracing platform of the Eclipse IDE and state-of-the-art model checker Spin.

We report on a tool for generating executable concurrent tests from scenarios specified as message sequence charts. The proposed approach features three steps: 1) Deriving a MSC test implementation from a MSC scenario, 2) Mapping the test implementation into a Promela model, 3) Generating executable test scripts in Java. The generation of an intermediate Promela model allows for model-checking to inspect the test implementation for properties like soundness, fault detection power as well as for consistency checking between different test scenarios. Moreover decoupling the executable test scripts from the scenario specification makes it possible to use different backend code generators to support other scripting languages when needed.

We present an automated framework for the inference of behavioral models from the execution traces of a web-based business application (WBA). The model inference framework consists of a formal approach to infer automata models from traces of WBA`s and an advanced prototype tool set implemented around the data mining engine Weka, the model checker SPIN, the formal language manipulation framework ANTLR and the graph visualization software GraphViz. The traces of a WBA are collected by monitoring the communications in client-server architectures, where a client can be an Internet browser or a service accessing the server side of the application. The inferred models depict both the control and data flow (showing data variations) of the WBA and can be used for its visualization and verification. Finally, we discuss Web-FIM an online deployment of the model inference framework and illustrate the use of the tools with an example.

We present an approach to the inference of automata models of web-based business applications using only execution traces recording the externally observable behavior of such applications. The proposed approach yields behavioral models representing both the control flow of an application and the data variations corresponding to different types of users. We also describe how the obtained models allow the use of verification techniques like model checking in the validation phase using a case study featuring a travel reservation agency.

We present a framework for property testing where a partially ordered execution trace of a distributed system is modeled by a collection of communicating automata. We prove that the model exactly characterizes the causality relation between the events in the observed trace. We present the implementation of this approach in SDL, where ObjectGEODE is used to verify properties, and illustrate the approach with an industrial case study.

The paper reports on an analysis technology based on the tracing approach to test trustworthy requirements of a distributed system. The system under test is instrumented such that it generates events at runtime to enable reasoning about the implementation of these requirements in a later step. Specifically, an event log collected during a system run is converted into a specification of the system. The (trustworthy) requirements of the system must be formally specified by an expert who has sufficient knowledge about the behaviour of the system. The reengineered model of the system and the requirement descriptions are then processed by an off-the-shelf model checker. The model checker generates scenarios that visualize fulfilments or violations of the requirements. A complex example of a concurrent system serves as a case study.

In this paper, we use supervisory control techniques to design a protocol converter, which avoids divergence in a communication systems. A typical application is to design gateways that interface heterogeneous computer networks while minimizing the communication time with the involved parties. As an example, we design a divergence-free converter that interfaces an alternating bit sender and a non-sequenced receiver, and we implement the converter as an asynchronous circuit.