Undervisningsplan

paper 1: Transition and Cancellation in Concurrency and Branching Time

paper 2: On the Expressiveness of Higher Dimensional Automata?

paper 1: HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems

slides of the presentation ?

Abstract:

In this talk I¡¯ll explain the coordination language, Reo. Then, I¡¯ll give an overview of its formal semantics, Constraint Automata. Some analysis techniques for Reo and Constraint Automata will be presented. ?

Abstract:

Testing real-time embedded systems (RTES) is in many ways challenging. Thousands of test cases can be potentially executed on an industrial RTES. Given the magnitude of testing at the system level, only a fully automated approach can really scale up to test industrial RTES. In this talk, I will describe a novel black-box testing approach and a methodology to model the RTES environment using the UML/MARTE/OCL international standards. The main motivation is to provide a more practical approach to the model-based testing of RTES by allowing system testers, who are often not familiar with the system design but know the application domain well enough, to model the environment to enable test automation. Environment models can support the automation of three tasks: the code generation of an environment simulator, the selection of test cases, and the evaluation of their expected results (oracles). Each of these tasks is complex, and poses several research questions that need to be addressed. Successful applications of the approach to two industries (WesternGeco and Tomra) will be discussed.?

Many complex continuous systems are modeled as non-linear autonomous systems, i.e., by a set of differential equations with one independent variable. Exact reachability, i.e., whether a given configuration can be reached by starting from an initial configuration of the system, is undecidable in general, as one needs to know the solution of the system of equations under consideration. In this paper we address the reachability problem of planar autonomous systems approximatively. We use an approximation technique which hybridizes the state space in the following way: the original system is partitioned into a finite set of polygonal regions where the dynamics on each region is approximated by constant differential inclusions. Besides proving soundness, completeness, and termination of our algorithm, we present an implementation, and its application into (classical) examples taken from the literature. ?

Abstract:

Synthesis of system configurations from a given set of features is an important and very challenging problem. This paper makes a step towards this goal by describing an efficient technique for synthesizing pipeline configurations of feature-based systems. We identify and formalize a design pattern that is commonly used in featurebased development. We show that this pattern enables compositional synthesis of feature arrangements. In particular, the pattern allows us to add or remove features from an existing system without having to reconfigure the system from scratch. We describe an implementation of our technique and evaluate its applicability and effectiveness using a set of telecommunication features from AT&T, arranged within the DFC architecture.

based on the paper?

Abstract:

An introduction to hybrid systems, the study of systems that have both discrete and continuous behavior.?

Modern software systems are increasingly being developed for deployment on a range of architectures. For this purpose, it is interesting to capture aspects of low-level deployment concerns in high-level modeling languages. In this paper, an executable object-oriented modeling language is extended with resource-restricted deployment components. To analyze model behavior a formal methodology is proposed to assess resource consumption, which balances the scalability of the method and the reliability of the obtained results. The main idea of our approach is to combine reliable (but expensive) worst-case cost analysis of statically predictable parts of the model with fast (but inherently incomplete) simulations of the concurrent aspects in order to avoid the state-space explosion. The approach is illustrated by the analysis of memory consumption.?