The Distributed and Embeeded Systems unit is running regular seminars where both local speakers as well as external visitors give talks on a wide range of topics from the concurrency theory and practice. The seminars are not only aimed at the local audience but also to any interested visitors from outside of the unit or the department.

Please contact Jiri Srba for information on the seminars in this series, and to be added to the mailing list for seminar announcements.

The schedule of past seminars can be found here.

 

7.2. 2012, 14:30, 0.2.11, Selma Lagerlöfs Vej 300
Cristiano Bertolini, Centre of Informatics (CIn), Federal University of Pernambuco (UFPE), Recife, Brazil
Grey-box GUI Testing

 Abstract: Graphical user interfaces (GUIs), due to their event driven nature, present a potentially unbounded space of all possible ways to interact with software. During testing it becomes necessary to effectively sample this space. In this talk we shall develop algorithms that sample the GUI’s input space by only generating sequences that (1) are allowed by the GUI’s structure, and (2) chain together only those events that have data dependencies between their event handlers. We create a new abstraction, called an event-dependency graph (EDG), of the GUI that captures data dependencies between event handler code. We develop a mapping between EDGs and an existing black-box user-level model of the GUI’s workflow, called an event-flow graph (EFG). We have implemented automated EDG construction in a tool that analyzes the byte code of each event handler.We evaluate our “grey-box” approach using four open-source applications and compare it with the current-state of-the-art EFG approach. Our results show that using the EDG reduces the number of test cases while still achieving at least the same coverage. Furthermore, we were able to detect one new bug in one of the subject applications.

 

 

17.11. 2011, 13:30, 0.2.12, Selma Lagerlöfs Vej 300
Manfred Droste, Automata and Formal Languages group, University of Leipzig, Germany
Weighted Automata and Quantitative Logics

 Abstract: In automata theory, a classical result of Buchi-Elgot-Trakhtenbrot states that the recognizable languages are precisely the ones definable by sentences of monadic second order logic. We will present a generalization of this result to the context of weighted automata. A weighted automaton is a classical non-deterministic automaton in which each transition carried a weight describing e.g. the resources used for its execution, the length of time needed, or its reliability. The behavior (language) of such a weighted automaton is a function associating to each word the weight of its execution. We develop syntax and semantics of a quantitative logic; the semantics counts 'how often' a formula is true. Our main results show that if the weights are taken either in an arbitrary semiring or in an arbitrary bounded lattice, then the behaviors of weighted automata are precisely the functions definable by sentences of our quantitative logic. The methods also apply to recent quantitative automata model of Henzinger et al. where weights of paths are determined, e.g., as the average of the weights of the path's transitions. Buchi's result follows by considering the classical Boolean algebra {0,1}. Joint work with Paul Gastin (ENS Cachan), Heiko Vogler (TU Dresden), resp. Ingmar Meinecke (Leipzig).

 

 

15.11. 2011, 10:00, 0.2.12, Selma Lagerlöfs Vej 300
Franck Cassez, CNRS, IRCCyN, Nantes, France
Computation of WCET using Program Slicing and Real-Time Model-Checking

 Abstract: Computing accurate WCET on modern complex architectures is a challenging task. This problem has been devoted a lot of attention in the last decade but there are still some open issues. First, the control flow graph (CFG) of a binary program is needed to compute the WCET and this CFG is built using some internal knowledge of the compiler that generated the binary code; moreover once constructed the CFG has to be manually annotated with loop bounds. Second, the algorithms to compute the WCET (combining Abstract Interpretation and Integer Linear Programming) are tailored for specific architectures: changing the architecture (e.g.,replacing an ARM7 by an ARM9) requires the design of a new ad hoc algorithm. Third, the tightness of the computed results (obtained using the available tools) are not compared to actual execution times measured on the real hardware. In the paper [Béchennec and Cassez: Computation of WCET using Program Slicing and Real-Time Model-Checking. Research report, IRCCyN, CNRS, Nantes, France, 2011, arXiv:1105.1633v2] we address the above mentioned problems. We first describe a fully automatic method to compute a CFG based solely on the binary program to analyse. Second, we describe the model of the hardware as a product of timed automata, and this model is independent from the program description. The model of a program running on a hardware is obtained by synchronizing (the automaton of) the program with the (timed automata) model of the hardware. Computing the WCET is reduced to a reachability problem on the synchronised model and solved using the model-checker Uppaal. Finally, we present a rigorous methodology that enables us to compare our computed results to actual execution times measured on a real platform, the ARM920T. The tools we use are: Uppaal and the GNU-ARM tool suite from CodeSourcery.

 

 

26.10. 2011, 14:30, 0.2.11, Selma Lagerlöfs Vej 300
Hans-Jörg Peter, Reactive Systems Group, Saarland University, Germany
Synthesizing Certificates in Networks of Timed Automata

 Abstract: We present automatic techniques for synthesizing monolithic and compositional correctness certificates in networks of timed automata. A correctness certificate is an easy-to-validate witness of the fact that a given system satisfies a certain property. We propose certificates to be small homomorphic (i.e., location-based) abstractions of the given system modeled as a network of timed automata. While a monolithic certificate is a timed automaton that simulates the whole network and still satisfies the property, a compositional certificate is an automaton that can transparently replace some selected components of the network during model checking. For obtaining monolithic certificates, we first present a symbolic abstraction refinement technique, enabling the combination of BDDs and DBMs. Then, we show how to obtain compositional certificates based on a forward and backward reachability analysis of (an abstraction) of the given system.

 

 

26.5. 2011, 13:00, 0.2.13, Selma Lagerlöfs Vej 300
Stefano Schivo, Formal Methods and Tools group, University of Twente, The Netherlands
Modeling Biological Pathway Dynamics with Timed Automata

 Abstract: In the last decade, biological experiments have been producing unbelievable quantities of data, which would be impossible to analyze without automatic assistance. Thus, bioinformatics is mainly focused on developing theories and tools for the analysis of large amounts of data. Nonetheless, it is also of primary importance to derive some theories from the available observations: modeling complex biological concepts can be of help in order to understand how what is observed works. If the models are based on computational assistance, they may offer the possibility to perform other experiments: the so-called "in-silico" experiments. In my presentation I will give an illustration about what biological signaling pathways are, and explain the current state of our effort towards a modeling environment which will hopefully allow biologists to obtain meaningful insights on the subject.

 

 

13.4. 2011, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Jörg Brauer, Embedded Software Laboratory, RWTH Aachen University, Germany
Automatic Abstraction for Binary Code Verification

 Abstract: Traditionally, abstractions have been manually designed for each operation in a program. Faithfully designing abstractions, however, is an arduous task when reasoning about binary code. This is due to the presence of logical (bit-wise) as well as arithmetic operations whose semantics is defined over machine integers of finite precision. Automatic abstraction provides a way to tame this complexity. This talk focuses on techniques for deriving invariants in terms of linear constraints. Such abstractions can be computed through incremental SAT solving if the concrete semantics of a program is described in propositional Boolean logic, a technique that is colloquially referred to as bit-blasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling integer overflows and underflows which arise in machine arithmetic.

 

 

6.4. 2011, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Nikola Benes, Masaryk University, Brno, Czech Republic
Process Algebra for Modal Transition Systemses

 Abstract: The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged. Therefore, we introduce transition system with obligations as a general model encompassing all the aforementioned models, and equip it with a process algebra description. Using these instruments, we then compare the previously studied subclasses and characterize their relationships.

 

 

30.3. 2011, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Jan Kretinsky, Masaryk University, Brno, Czech Republic and Technical University Munich, Germany
Disjunctive Modal Transition Systems and Generalized LTL Model Checking

 Abstract: Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify a fundamental error made in previous attempts at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME.

 

 

23.3. 2011, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Saleem Vighio , Department of Computer Science, Aalborg University, Denmark
Modelling and Verification of Web Services Business Activity Protocol

 Abstract: In this talk, I present formal analysis of WS-Business Activity with Coordination Completion (BAwCC) protocol using the model checker Uppaal. We analyse various communication policies of the protocol and our analysis reveals that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modifieded protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behavior is preserved. Another important property of communication protocols is that all parties always reach their final states. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not.

 

 

17.3. 2011, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Michel Reniers, Department of Mechanical Engineering, Eindhoven University, Netherlands
A Process-Algebraic Approach to Supervisory Control Theory

 Abstract: We revisit the central notion of controllability in supervisory control theory from a process-theoretic perspective. To this end, we investigate a behavioral preorder that is coarser than bisimulation and finer than simulation. It is parameterized by a set of actions that need to be bisimulated, whereas the other actions only need to be simulated. This preorder provides a viable means to define controllability in a nondeterministic setting as a refinement relation on processes. The new approach provides for a generalized characterization of controllability of nondeterministic discrete-event systems. We characterize the existence of a deterministic supervisor.

 

 

11.2. 2011, 10:00, 0.2.11, Selma Lagerlöfs Vej 300
Carsten Fuhs, RWTH Aachen University, Germany
SAT Encodings: From Automated Termination Analysis to Program Synthesis

 Abstract: Over the last years, fully automated modular and incremental termination proofs using ad hoc abstractions for the proof obligations at hand have become commonplace in the area of term rewriting. Being a syntactically simple yet expressive Turing-complete language, term rewriting is nowadays used as a backend language also for analysis of programs from real-life programming languages such as Haskell, Prolog, or Java Bytecode. These success stories are due to SAT-based techniques to automate the search for suitable abstractions driving the termination proof effort. We present how highly efficient SAT solvers in combination with carefully tuned SAT encodings render automated abstraction techniques scalable to large examples. However, the usefulness of SAT-based techniques is not limited to automated abstraction and verification. In recent work, we have applied our experience in devising SAT encodings to automate synthesis of optimal Boolean XOR straight-line programs, which typically arise e.g. in implementations of symmetric ciphers. While the resulting SAT instances often tend to be surprisingly hard, we have obtained a SAT-based optimality proof for an important part of the Advanced Encryption Standard (AES).

 

 

24.11. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Peter Bulychev, Department of Computer Science, Lomonosov Moscow State University, Russia
Detection of software clones. Universal simulation checking tool.

 Abstract: My talk will consist of two unrelated parts. In the first part I'll talk about detection of software clones. Software clone consists of a pair of code fragments that are large and similar enough. The presence of clones can increase software maintenance cost and thus it is important to detect them. I will talk about abstract syntax tree-based clone detection tool Clone Digger (http://clonedigger.sf.net), that I have developed. In the second part I'll talk about game-theoretic simulation checking approach. I'll describe my BDD-based tool that is able to check various simulation relations between finite Kripke structures.

 

 

29.9. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Wang Zheng, Software Engineering Institute, East China Normal University, China
Automatically Checking and Testing Web Service Choreography

 Abstract: Web Service Choreography Description Language gives a global view on the collaborations among a collection of services involving multiple participants or organizations. WS-CDL specification regulates the correct behaviors a WS-CDL document has to obey. Thus, constraints are specified in WSCDL specification including static, dynamic and implementation ones. We developed a relational calculus to capture those static constraints precisely and a corresponding algorithm to check if a WS-CDL document satisfying those constraint. We present an approach based on symbolic execution to test WS-CDL document. Moreover, a simulation engine for WS-CDL is used to perform the execution of WS-CDL documents during the process of symbolic execution. Dynamic and implementation constraints in WS-CDL specification are checked during simulation.

 

 

15.9. 2010, 15:00, 0.2.90, Selma Lagerlöfs Vej 300
Romain Sertelon, SUPINFO - The International Institute of Information Technology, France
Parameterized UPPAAL

 Abstract: In this work we present a Ruby on rails server designed to drive parameterized model-checking on a cluster using UPPAAL as the back-end model-checker. The approach is general and applies to any model-checker. In addition, the framework allows for customized exploration strategies, e.g., genetic algorithms, to explore the parameter space. The feedback is planned to be through a Java applet to show the results graphically.

 

 

15.9. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Lasse Jacobsen, Department of Computer Science, Aalborg University, Denmark
A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

 Abstract: Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.

 

 

28.4. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Li Guangyuan, Institute of Software, the Chinese Academy of Sciences, Beijing, China
Model Checking Time-Constraint LTL Properties for Timed Automata

 Abstract: Time-constraint LTL is an extension of propositional linear temporal logic (LTL) with atomic clock constraints added as atomic formulas. It also can be regarded as a linear-time version of the requirement specification language of Uppaal. This talk will describe an automata-theoretic approach via automata emptiness for model checking time-constraint LTL properties of timed automata. We will show that time-constraint LTL formulas can be translated into time-constraint Buchi automata, which are a special subclass of timed Buchi automata. By combining this translation procedure with our previous zone-based emptiness checking procedure for timed Buchi automata, a tool called CTAV for model checking time-constraint LTL properties for timed automata has been implemented.

 

 

8.4. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Jüri Vain, Tallinn University of Technology, Estonia
Driving On-line Testing with Reactive Planning

 Abstract: We describe a method and algorithm for model-based construction of an on-line reactive planning tester (RPT) for black-box testing of embedded systems specified by non-deterministic extended finite state machine (EFSM) models. The key idea of RPT lies in off-line learning of the System Under Test (SUT) model to prepare the data for efficient on-line reactive planning. A test purpose is attributed to the transitions of the SUT model by a set of Boolean conditions called traps. The result of the off-line analysis is a set of constraints used in on-line testing for guiding the SUT towards taking the moves represented by trap-labelled transitions in SUT model and generating required data for inputs. We discuss the practical usage of RPT for systems with high degree of non-determinism, deep nested control loops, and requiring bounded tester response time.

 

 

26.1. 2010, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Mohammad Mahdi Jaghoori, Centrum voor Wiskunde en Informatica (CWI), Netherlands
Schedulability Analysis of Concurrent Objects

 Abstract: Correct performance of a real-time application and its QoS properties crucially depend on the strategy for scheduling of its processes. However, traditional approaches to software development defer scheduling issues to the operating system. In contrast, we integrate scheduling policies into the object modeling process itself. We employ timed automata and Uppaal to verify the schedulability of concurrent objects in isolation w.r.t their behavioral interfaces. Then with our notion of refinement for timed automata, we define the compatibility of the concurrent objects in a system such that the schedulability of the entire system can be tested.

 

 

11.12. 2009, 10:00, 0.2.90, Selma Lagerlöfs Vej 300
Ernst-Rüdiger Olderog, Department of Computer Science, University of Oldenburg, Germany
Towards Decomposition Theorems for Lane Change Assistance Systems

 Abstract: In our previous work with W. Damm and H. Hungar we proposed a proof rule for the collision freedom of two traffic agents, with instantiations to car and train scenarios. The proof rule exploits a design pattern for the interaction of controllers of the traffic agents. In this talk we consider collision freedom for many cars that drive on a multi-lane motorway and perform lane change maneuvers. We are developing conditions for cooperative lane change assistance systems for cars such that the collision freedom can be established by decomposition and reuse of the previous proof rule. The talk is based on research on hybrid systems carried out in the Trans-regional Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbrücken.

 

 

27.11. 2009, 13:00, 0.2.13, Selma Lagerlöfs Vej 300
Axel Legay, INRIA, Rennes, France
Statistical Model Checking

 Abstract: Given a stochastic system (a Markov Chain,...), the probabilistic model checking problem consists in deciding whether this system satisfies some property with a probability greater or equal to a certain threshold. There exist several numerical algorithms (implemented in tools such as PRISM or LIQUOR) for solving such problems. Unfortunately, those algorithms do not scale up to realistic systems. In this talk, we will show that techniques coming from the area of statistics can be used to solve the probabilistic model checking problem. Contrary to numerical algorithms, those statistic algorithms are applicable to realistic systems. In this talk, we will consider the application of statistical model checking to two families of systems, namely digital/analog circuits and systems biology. We will also briefly introduce Bayesian model checking (particularly suited for systems biology).

 

 

7.10. 2009, 15:00, 0.2.90, Selma Lagerlöfs Vej 300
Anders Møller, Department of Computer Science, Aarhus University, Denmark
Type Analysis for JavaScript

 Abstract: JavaScript is the main scripting language for Web browsers, and it is essential to modern Web applications. Programmers have started using it for writing complex applications, but there is still little tool support available during development. This talk presents a static program analysis infrastructure that can infer detailed and sound type information for JavaScript programs using abstract interpretation. The analysis is designed to support the full language as defined in the ECMAScript standard, including its peculiar object model and all built-in functions. The analysis results can be used to detect common programming errors or rather, prove their absence, and for producing type information for program comprehensio.

 

 

23.9. 2009, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Sandie Balaguer, Ecole Centrale de Nantes, France
Specification and Verification of Properties Using Live Sequence Charts

 Abstract: Live Sequence Charts (LSCs) are a powerful visual language which can express enriched requirements and extend the UPPAAL requirement specification language. We reduce the problem of checking if a system satisfies a property specified as an LSC scenario to checking a "leads-to" property in UPPAAL. This is done by adding observers to the original model and verifying a liveness property for the observers. The verification engine automatically augments the systems with these observers and the graphical interface supports LSCs.

 

 

18.9. 2009, 13:00, 0.2.12, Selma Lagerlöfs Vej 300
Aske Brekling, Technical University of Denmark, Denmark
MoVES timed-automata modelling and verification of embedded systems (clocks, stopwatches and without clocks)

 Abstract: The "Modelling and Verification of Embedded Systems" (MoVES) framework is being developed to assist in embedded systems design. The framework can be used to conduct schedulability analysis and has the potential to reason about different types of resource usage such as memory usage and power consumption. The framework consists of a simple specification language for embedded systems as well as different Uppaal templates that can be used to instantiate specified systems. Schedulability analysis in terms of deadline detection and analysis of resource usage of specified systems can be analyzed using the Uppaal verification engine. A basic overview of the different Uppaal templates and their structure will be presented. Specifically the different uses of Uppaal - models with normal clocks, models with stop watches and models without clocks - will be shown. Also, small experiments will indicate how the MoVES framework can be used and possibly extended. A system specified in MoVES is specified as a platform specification, an application specification and a mapping of the application onto the platform. An application consists of a number of tasks and a task graph describing data dependencies. The second part of the talk can help to understand what a task could be and what properties such as best-/worst case execution times are. The third part of the talk deals with analysis of quantitative properties of hardware specifications Gezel provides a much needed level of abstraction in hardware specifications and is extremely helpful in giving some clear insight in design processes. However, as Gezel has no formal semantics it can be difficult to get a deep understanding of many of the constructs in the language. Here, a compositional semantic domain for Gezel aiming at automated verification will be presented. Demonstrations of how the semantic domain can be used to do verification of underlying algorithms will be shown. This verification is conducted by generating Uppaal models for hardware specifications which follows from the semantic domain. Furthermore, experimental results using the formalisms of the semantic domain to analyze quantitative properties of hardware specifications such as time and space.

 

 

9.9. 2009, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Guadalupe Ortiz, Centro universitario de Mérida (University of Extremadura), Spain
Integrating Extra-Functional Properties in Web Service Model-Driven Development

 Abstract: In the last few years, model-driven architecture, aspect-oriented software development and Web service engineering have become widely accepted alternatives for tackling the design and building of complex distributed applications. Although these methodologies have the principle of separation of concerns and their further integration as a key factor in obtaining high-quality and evolvabledistributed systems, they usually address this principle from their own perspective. Our view is that, when combined appropriately, both model-driven and aspect-oriented software development may complement each other to develop high-quality Web service-based systems, maintaining their extra-functional properties separate from models to code. In particular, we provide a methodology that integrates extra-functional properties into web service model-driven development. The resulting approach increases the modularity and encapsulation of the different modules, thus reducing implementation and maintenance costs and keeping properties traceability at all stages of development. With this purpose, a set of metamodels and transformation rules has been created to be integrated with the ATLAS eclipse plugin. The developed experimental results have shown that the use of aspect-oriented techniques does not result in runtime penalty and that a lot of workload is saved when automatically generating a well-structured skeleton for the application.

 

 

29.5. 2009, 13:00, 0.2.90, Selma Lagerlöfs Vej 300
Andrei Sabelfeld, Chalmers University of Technology, Sweden
A Classification of Declassification

 Abstract: Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognized the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released, and when information can be released. We apply this classification in order to evaluate the security of a case study realized in a security-typed language -- an implementation of a non-trivial cryptographic protocol that allows playing online poker without a trusted third party. In addition, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful "sanity checks" for emerging models. The talk is based on joint work, in part, with David Sands, and, in part, with Aslan Askarov.

 

 

1.5. 2009, 10:00, 0.2.90, Selma Lagerlöfs Vej 300
Gerrit Muller, Buskerud University College, Norway
BODERC Presentation

 Abstract: The development of high volume office printers requires a tight cooperation of many disciplines, such as mechanical engineering, control engineering and software engineering. Problems arise in practice at the borders between these disciplines.
Boderc was a 5 year research project where modeling is proposed as solution for the stagnating cooperation between these disicplines. The project was staffed with 6 PhD's from software electrical, control, and mechanical engineering, plus 4 engineers from industry and 2 research fellows. This team build many models and evaluated these models in the industrial context. We will discuss the results of the projects and the lessons learned.

 

 

11.11. 2008, 11:00, 0.2.90, Selma Lagerlöfs Vej 300
Christian Engel, Universität Karlsruhe, Germany
Deductive Verification of RTSJ Programs

 Abstract: The Real-Time Specification for Java (RTSJ) defines a region-based memory model with the capability to explicitely free memory regions (so called scoped memory areas). For preventing dangling references it introduces runtime checks, raising errors in the case of a failure, to constrain the creation of references between objects residing in different regions. We present how an existing dynamic logic calculus for Java is extended to handle RTSJ’s memory model, thus enabling to prove the absence of failed runtime checks. This is crucial for giving safety guarantees for RTSJ applications or could allow the Java Virtual Machine (JVM) to skip these kind of runtime checks resulting in improved performance.
Another specialty of RTSJ is the absence of garbage collection in scoped memory areas. This necessitates precise estimations for the required size of scoped memory ares. If these estimations are incorrect, i.e. lower than the actual worst case memory usage (WCMU) of an application in one of the respective scopes, OutOfMemoryErrors can render the regarded application erroneous. Thus another goal of formal verification of RTSJ programs is to ensure the correctness of given WCMU estimates and thus the absence of OutOfMemoryErrors. We propose a contract-based approach for this which facilitates modularity of the applied analysis.

 

 

15.10. 2008, 11:00, 0.2.13, Selma Lagerlöfs Vej 300
Rodolfo Gomez, The Computing Lab at the University of Kent, UK
Modeling Timed Automata with Deadlines in Uppaal

 Abstract: Timed Automata with Deadlines (TAD) is a notation to model concurrent real-time systems that has a number of advantages over mainstream Timed Automata (TA). TAD provide more natural primitives to model urgent actions and avoid the occurrence of (the most common form of) timelocks. We show how TAD can be modeled in Uppaal, one of the most widely used model-checkers for TA. The techniques presented here allow users to benefit from Uppaal's GUI, modeling facilities and efficient verification algorithms to construct and analyze TAD.

 

 

24.9. 2008, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Antoine Hom, Ecole Centrale Nantes, France
The New Engine of UPPAAL-TIGA with Partial Observability

 Abstract: Abstract: In 2007 we presented an algorithm for solving timed games with partial observability. The algorithm was implemented in Ruby and this early prototype ONLY allowed us to perform very limited experiments. In this work we present different optimizations on the original algorithm and its implementation in the tool UPPAAL-TIGA.

 

 

25.6. 2008, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Simon Tschirner, Department of Information Technology, Uppsala University, Sweden
Model-Based Validation of QoS Properties of Biomedical Sensor Networks

 Abstract: We present a formal model of a Biomedical Sensor Network whose sensor nodes are constructed based on the IEEE 802.15.4 / ZigBee standard for wireless communication. We have used the UPPAAL tool to tune and validate the temporal configuration parameters of the network in order to guarantee the desired QoS properties for a medical application scenario. The case study shows that even though the main feature of UPPAAL is model checking, it is also a promising and competitive tool for efficient simulation.

 

 

19.6. 2008, 13:00, 0.2.13, Selma Lagerlöfs Vej 300
Jan Midtgaard, IRISA / INRIA Rennes, France
A Calculational Approach to Control-Flow Analysis by Abstract Interpretation

 Abstract: We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a demand-driven 0-CFA. We thereby provide a novel characterization of the analysis.

 

 

16.4. 2008, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Martin Schoeberl, Real Time Systems Group, Vienna University of Technology, Austria
JOP, a Java Processor for Embedded Real-time Systems

 Abstract: Java is getting more and more popular for embedded systems development. In resource constraint environments a direct implementation of the JVM in hardware - a Java processor - is an interesting option. In this talk I will present the architecture of JOP, the Java Optimized Processor, and it's implementation in an FPGA. JOP is designed for time-predictable execution of JVM bytecodes to ease worst-case execution time (WCET) analysis. I will also present two future trends in the context of Java processors: (1) the upcoming specification for Safety Critical Java, and (2) a path to chip multiprocessing for real-time Java.

 

 

28.11. 2007, 14:00, 0.2.13, Selma Lagerlöfs Vej 300
Uli Fahrenberg, Department of Computer Science, Aalborg University, Denmark
"Inverse semantics" for Timed Automata

 Abstract: We are concerned with the question which properties a timed transition system should forfill for it to occur as the semantics of a timed automaton. This is an interesting question for example when one tries to "lift" the open maps formalisms of Joyal, Nielsen and Winskel to timed automata. In this talk, we shall give some motivation for this problem, with the above application in mind, and present a theorem which solves it.
The talk will be split in two parts. In the first part, approx. 30 min, I will give a gentle introduction to the beauty and usefulness of open maps, motivate the general problem of "lifting" open maps across different formalisms, and state the theorem. After a short break, I will give a detailed proof of the theorem; this second part will last approx. 45 min.

 

 

14.11. 2007, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Rene Rydhof Hansen, Department of Computer Science, Aalborg University, Denmark
Non-Interference for Java Card Bytecode

 Abstract: Non-interference is the property of a program not to leak any secret information. In this talk I propose a notion of non-interference for an abstract bytecode language, based on Java Card bytecode, that is more granular than the class based non-interference often proposed for object-oriented languages. A static information flow analysis for automatically verifying that a program has the non-interference property is developed; the soundness proof for the analysis is briefly covered. Finally, a notion of non-interference based "simple erasure policies" are defined.

 

 

7.11. 2007, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Martin Kot, Centre for Applied Cybernetics, Technical University of Ostrava, Czech Republic
Modeling and Verification of Real-Time Database Management Systems in Uppaal

 Abstract: Real-time database management systems (RTDBMS) are recently subject of an intensive research. Many different protocols, algorithms and policies were suggested for particular parts of RTDBMS. Model checking algorithms and verification tools are of great concern as well. I will talk about my effort to use a verification tool Uppaal on some concurrency control protocols used in real-time database management systems. I will show some possibilities of modeling such protocols using nets of timed automata, which are a modeling language of Uppaal. Then I will describe results of my model checking attempts on those models.

 

 

24.10. 2007, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Jiri Srba, Department of Computer Science, Aalborg University, Denmark
Can UPPAAL Verify a Petri Net Extended with Time Features?

 Abstract: A timed extension of Petri nets where every token has an associated age from the domain of real numbers is a well-studied formalism for modelling of real-time systems. Unfortunately, there is no tool support for the verification of such nets yet. In this talk I will describe mutual translations between the timed extension of Petri nets and the model of timed automata as used e.g. in the verification tool UPPAAL. A prototype tool with GUI translating Petri net verification questions to UPPAAL-ready timed automata will be presented, including some preliminary experimental results.

 

 

27.9. 2007, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Quentin le Burel, Ecole Centrale de Nantes, France
Improving the Strategies of UPPAAL-TIGA

 Abstract: UPPAAL-TIGA implements the first efficient on-the-fly reachability algorithm for timed games presented at Concur'05. The prototype matured to an efficient tool in 2006 when it was rewritten based on the UPPAAL architecture. This year the tool has been improved with respect to its strategies. We have solved the problem of interactive play of the strategy from our GUI or the command line. Furthermore, the strategy is now available as a hybrid multi-terminal BDD/CDD. This allows further developments with a more compact representation of the strategy for code generation.

 

 

19.9. 2007, 13:00, 0.2.13, Selma Lagerlöfs Vej 300
Ulrik Nyman, Center for Embeeded Software Systems, Aalborg University, Denmark
Modal Transition Systems

 Abstract: Almost 20 years after the original conception, we revisit several fundamental question about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement using a counterexample due to Huttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations) for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizing implementations, together with their complexities.

 

 

15.5. 2007, 11:00, E3-109, Fr. Bajersvej 7E
David N. Jansen, RWTH Aachen, Germany
Probably on Time and Within Budget

 Abstract: "PPTA'' extend timed automata with both prices (on edges and locations) and discrete probabilities. I will show an algorithm that calculates whether the probability to reach a goal location within a given price and time bound is larger than a predetermined probability threshold. The algorithm is partially correct, but unfortunately provides only a semi-decision.

 

 

2.5. 2007, 14:30, B2-109, Fr. Bajersvej 7B
Mani Swaminathan, Oldenburg University, Germany
A Symbolic Decision Procedure for Robust Safety of Timed Systems

 Abstract: We present a symbolic algorithm for deciding safety (reachability) of timed systems modelled as Timed Automata (TA), under the notion of robustness w.r.t infinitesimal clock-drift. The algorithm uses a "neighbourhood'' operator on zones that is efficient to compute. In contrast to other approaches for robustly deciding reachability of TA, which are either region based (Puri, 2000), (DeWulf, Doyen, Markey, and Raskin, 2004), or involve a combination of forward and backward analyses when zone-based (Daws and Kordy, 2006), ours is a zone-based fully forward algorithm that is guaranteed to terminate, and requires no special treatment of cycles. Our notion of robustness is weaker than the classical definition, but is nonetheless realistic in the sense that it can be applied to all systems that have a bounded life-time. An interesting consequence is that the standard Forward Reachability Analysis algorithm used in tools such as UPPAAL is in fact robust under our notion for closed TA and closed target states.

 

 

18.4. 2007, 14:30, A4-106, Fr. Bajersvej 7B
Alexandre David, Department of Computer Science, Aalborg University, Denmark
UPPAAL-Tiga: Past, Present, and Future!

 Abstract: The first prototype of UPPAAL-Tiga was born in 2005 when we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. Since then the prototype has matured to a fully integrated tool with dramatic improvements both in terms of performance and the availability of the extended input language of UPPAAL 4.0. In this talk I will present the foundations of the tool, its overall design, and the new features in development.

 

 

14.3. 2007, 14:30, A4-106, Fr. Bajersvej 7B
Ulrik Nyman, Department of Computer Science, Aalborg University, Denmark
Modal I/O Automata for Interface and Product Line Theories

 Abstract: Alfaro and Henzinger use alternating simulation in a two player game as a refinement for interface automata. We show that interface automata correspond to a subset of modal transition systems of Larsen and Thomsen, on which alternating simulation coincides with modal refinement. As a consequence a more expressive interface theory may be built, by a simple generalization from interface automata to modal automata. We define modal I/O automata, an extension of interface automata with modality. Our interface theory that follows can express liveness properties, disallowing trivial implementations of interfaces, a problem that exists for theories build around simulation preorders. In order to further exemplify the usefulness of modal I/O automata, we construct a behavioral variability theory for product line development.

 

 

21.2. 2007, 14:30, B2-109, Fr. Bajersvej 7B
Hans Søndergaard, University College - Vitus Bering, Denmark
Real-Time Java for Embedded Systems

 Abstract: Nearly since Java emerged about 13 years ago, the discussion about "Java and Real-time" has taken place. Some of the strenghts of standard Java (multi-threading and garbage collection, for example) make it useless for hard real-time systems. However, the benefits of Java together with an appropriate Real-Time Java profile make Java an attractive language for real-time systems.

Three Real-Time Java profiles will be presented and discuss

• The Real-Time Specification for Java (RTSJ), appearing in 1999
• The Ravenscar-Java Profile, first proposed in 2001
• The Safety Critical Java Specification, JSR-302, started 2006 by a SUN Expert Group. 

 

We will conclude by telling how CISS is involved doing research into the above mentioned specifications. Our newest project is called JLAB (Java Lab for Embedded Systems).

 

 

14.2. 2007, 14:30, C2-209, Fr. Bajersvej 7B
Jacob Gorm Hansen, University of Copenhagen, Denmark
The Laundromat Model for Autonomic Cluster Computing

 Abstract: Traditional High Performance Computing systems require extensive management and suffer from security and configuration problems. This talk presents a new cluster management system called Evil Man. Evil Man is inspired by real-life Laundromats: All nodes in a cluster are configured with a minimal software base consisting of a Virtual Machine Monitor and a remote bootstrapping mechanism, and customers then buy access using a simple pre-paid token scheme. All necessary application software, including the operating system, is provided by the customer as a full Virtual Machine, and boot-strapped or migrated into the cluster as needed.
Technically, the core ingredients of Evil Man are a novel operating system Boot-strapping and Self-Migration mechanism, and a simple pre-paid Token Scheme on which all access control and accounting is based. Combined, these mechanisms create a simple, autonomous, secure, and highly flexible cluster computing platform suitable for deployment in a cluster or Grid system. We work hard at reducing the amount of privileged network-facing software on each node. For instance, the privileged part of our network protocol implementation consists of only a few hundred lines of C-code.
In this talk I will present the Evil Man system, and describe the novel Self-migration mechanism on which it is based. I will also outline my future visions for the work, and discuss other subjects related to operating systems and system security.

 

 

7.2. 2007, 14:30, B2-109, Fr. Bajersvej 7B
Goran Frehse, Verimag - UMR Universite Joseph Fourier/CNRS/INPG , France
PHAVer: Sound Reachability Analysis for Hybrid Systems

 Abstract: Embedded controllers can exhibit complex behavior because instantaneous, event-driven changes may interact with the continuous, time-driven evolution of the physical environment in ways that are difficult to predict. Because of their mixed discrete-continuous nature, such systems are called hybrid. One can make guarantees about certain properties of a hybrid system (such as bounds on the variables or on the cycle time of an oscillator circuit) by computing the set of reachable states. Our tool PHAVer does this for hybrid systems with affine dynamics in a formally, i.e., algorithmically as well as numerically, sound way. By partitioning the state space and computing piecewise constant bounds on the derivatives for each partition, the reachable states can be efficiently computed with geometric operations on polyhedra. In this talk, we present PHAVer's reachability algorithm and crucial improvements such as complexity for polyhedra, directing the search based on a topological sort, and forward/backward-refinement. The approach is illustrated with benchmark examples, amongst others a voltage controlled oscillator circuit and a chemical plant that were previously beyond the capabilities of verification tools. PHAVer is available at www.cs.ru.nl/~goranf/.

 

 

24.1. 2007, 12:30, A4-108, Fr. Bajersvej 7B
Luo Yigui, Tongji University, China
Developing more Cost-Efficient and more Dependable Embedded Systems

 Abstract: I am going to make a presentation about what I have been doing during the past few years and what I want to do in CISS in the following few months. The first project that I will introduce was cooperated with Darmstadt University of Technology. It includes the Co-Design Model (CDM), the co-synthesis framework, and the Dual Transition Timed Petri Net (DTTPN), and etc. The second one is about an IP core design with non-trivial real-time constraints. And some other improvement on Linux will also be presented.

 

 

13.12. 2006, 14:30, A4-106, Fr. Bajersvej 7B
Piotr Kordy, Formal Methods and Tools Group, University of Twente, Netherlands
Symbolic Robustness Analysis of Timed Automata

 Abstract: We propose a symbolic algorithm for the analysis of the robustness of timed automata. The robustness problem appears when we allow small drifts on the clocks or the imprecision on guards. If we allow imprecision the set of reachable states is different from normal reachability, even if imprecision is infinitely small. Puri presented algorithm to find a reachable set of states based on regions. Our algorithm extends Puri's algorithm but is based on zones. It relies on computation of stable zone for each cycle of timed automaton. . The stable zone is the largest set of states that can reach and be reached from itself through the cycle. To compute the robust reachable set, each stable zone that intersects the set of explored states has to be added to the set of states to be explored.

 

 

29.11. 2006, 14:30, B2-109, Fr. Bajersvej 7B
Jiri Srba, Department of Computer Science, Aalborg University, Denmark
Verification Techniques for Visibly Pushdown Automata

 Abstract