Previous seminars (2006-2014)

27.11. 2014, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Christophe Chareton, Onera, Toulouse, France, Formal modelling of requirements and temporal multi-agent logics

 Abstract: These works concern formal modelling of requirements and interactions between agents. We develop a modelling language for the requirements of a system to be elaborated, Khi. We also propose a temporal multi-agent logic, USL. To our knowledge, there is no formalisation, in the field of requirements engineering, dealing on the one hand with time and on the other hand with agents actions. This is what we propose with Khi. This language borrows from the Kaos method it means for the formally describing behavioral requirements and deriving from these requirements the operations specifications for a system. It also borrows from the Tropos-i* methods a conceptual frame enabling to express the question of the effective capacity of agents to ensure the satisfaction of the specifications assigned to them. We call this last question the "assignment problem". Thus, language Khi proposes an original synthesis enabling to formalise in an unique language the behavioral requirements of a system and the actions capacities of the agents in this system. Furthermore, Khi offers a conceptual frame enabling to express the assignment problem. To give Khi concepts a formalism and some means to solve the assignment problem, we also introduce a a temporal multi-agent logic, USL. IT is inspired from works in the domain such as ATLsc and SL. As these last formalisms, USL makes use of strategy contexts to express capacities of agents to ensure the satisfaction of temporal properties. USL is different from other existing formalisms by two mains aspects: first it uses non-deterministic strategies. We call them multi-strategies. So we can express properties of multi-strategy refinment. Furthermore, for USL we use executions in the system that may not be infinite. Thus we can formalise the notions of contradictory commitments for an agent and conflictual capacities of actions for a set of agents. We show that the expressivity of USL embeds the expressivity of pre-existing formalisms. This logic enables in particular to formalise the property, new in the field, of sustainable controle. It also enables to introduce predicates of comparison and equality between multi-strategies and/or strategies. A study of relations of dependencies between multi-strategies and/or strategies is also initiated with USL. We also show that the complexity of model-checking and satisfiability problems for USL is equivalent to that for pre-existing formalisms. Then we reduce the satisfaction of correction criteria expressing the assignment problem in Khi to instances of model-checking in an adequate version of USL, USLKhi. We give a resolution algorithm for this problem, it use a polynomial space. So, the development of Khi and the adequate use of USL enable to express, formalise and resolve the assignment problem. All these concepts is also illustrated by use of a case study figuring missions of spatial observations.

12.11. 2014, 14:30, 0.2.13, Selma Lagerlöfs Vej 300
Nikola Benes, Faculty of Informatics, Masaryk University, Brno, Czech Republic
On Clock-Aware LTL Properties of Timed Automata

 Abstract: We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique. The technique is implemented within the parallel and distributed model checker DIVINE.

27.8. 2014, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Simon Laursen, Department of Computer Science, Aalborg University, Denmark
Synchronization under Partial Observability

 Abstract: Embedded devices usually share only partial information about their current configurations as the communication bandwidth can be restricted. Despite this, we may wish to bring a failed device into a given predetermined configuration. This problem, also known as resetting or synchronizing words, has been intensively studied for systems that do not provide any information about their configurations. In order to capture more general scenarios, we extend the existing theory of synchronizing words to synchronizing strategies, and study the synchronization, short-synchronization and subset-to-subset synchronization problems under partial observability. We provide a comprehensive complexity analysis of these problems, concluding that for deterministic systems the complexity of the problems under partial observability remains the same as for the classical synchronization problems, whereas for nondeterministic systems the complexity increases already for systems with just two observations, as we can now encode alternation.

22.8. 2014, 13:30, 0.2.90, Selma Lagerlöfs Vej 300
Kim G. Larsen, Department of Computer Science, Aalborg University, Denmark
On Time with Minimal Cost!

 Abstract: (Priced) timed games are two-player quantitative games involving an environment assumed to be completely antogonistic. Classical analysis consists in the synthesis of strategies ensuring safety, time-bounded or cost-bounded reachability objectives. Assuming a randomized environment, the (priced) timed game essentially defines an infinite-state Markov (reward) Decision Process. In this setting the objective is classically to find a strategy that will minimize the expected reachability cost, but with no guarantees on worst-case behaviour. In this work, we provide efficient methods for computing reachability strategies that will both ensure worst case time-bounds as well as provide (near-) minimal expected cost. Our methods extend the synthesis algorithms of the synthesis tool Uppaal-Tiga with suitable adapted reinforcement learning techniques, that exhibits several orders of magnitude improvements w.r.t. previously known automated methods. Joint work with: Alexandre David, Peter G. Jensen, , Axel Legay, Didier Lime, Mathias G. Sørensen, and Jakob H. Taankvist

22.8. 2014, 12:30, 0.2.90, Selma Lagerlöfs Vej 300
Jan Kretinsky, IST, Austria
New Views on Probabilistic Systems Analysis

 Abstract: In the first part, we give a natural definition of bisimulation on probabilistic systems that are understood not as stochastic processes, but rather as transformers of probability distributions. Several examples demonstrate the use of the definition. We also give algorithms for computing this bisimulation not only for finite, but also for classes of uncountably infinite systems. In the second part, we show how machine-learning techniques can be applied in verification of Markov decision processes (MDPs). The first application is the first statistical model checking algorithm for unbounded properties in MDPs. The second application is improving performance of the standard algorithms by avoiding an exhaustive exploration of the state space, yielding precise lower and upper bounds on the required probability. Experimental results show a significant speed up.

15.8. 2014, 13:00, 0.2.90, Selma Lagerlöfs Vej 300
Sine Viesmose Birch, Department of Computer Science, Aalborg University, Denmark
Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets

 Abstract: State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or an over-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL and demonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.

9.4. 2014, 14:30, 0.2.11, Selma Lagerlöfs Vej 300
Peter Gjoel Jensen, Department of Computer Science, Aalborg University, Denmark
Memory Efficient Data Structures for Explicit Verification of Timed Systems

 Abstract: Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however,at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.

26.11. 2013, 13:00, 0.2.90, Selma Lagerlöfs Vej 300
Nikolaj Bjorner, Microsoft Research, Redmond, USA
The Satisfiability Modulo Theories solver Z3

 Abstract: Automated reasoning has become an integral part of software engineering tools in recent years thanks to high-performance theorem provers. The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, Pex, Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Spec Explorer, SecGuru, and Terminator. These tools reduce program analysis, verification and testing problems to logic queries that are solved using Z3. The talk takes these applications of Z3 as a starting point and examines applications SAGE, Dafny and SecGuru in some more depth. SAGE uses dynamic symbolic execution. It has been used to eradicate hundreds of security vulnerabilities in media readers that are otherwise well-known to be prone to security critical bugs. Dafny is a program verification environment and presents the current state-of-the-art in program verification methodologies and tools. SecGuru is a tool for automatically validating network connectivity restriction policies in large scale data-centers such as Windows Azure. We then describe some of the current trends in Z3: including solving recursive Horn clauses, solving real and floating point arithmetic.

5.3. 2014, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Krzysztof Czarnecki, Electrical and Computer Engineering, University of Waterloo, Canada
Upgradable Car: Towards An Extensible Automotive Systems and Software Architecture

 Abstract: With hundreds of sensors, multiple networks, and close to one hundred processors, modern automobiles are becoming smart, location-aware mobile platforms on wheels. The advent of vehicle-to-vehicle communication and autonomous driving heralds even stronger computerization of cars in the future. However, given today’s long development cycles of four to five years and a typical length of car ownership ranging from five to ten years, the computers and software embedded in cars become quickly outdated, especially by technology standards set by smart phones. Current automotive systems and software architectures, including the recently introduced Automotive Open System Architecture (AUTOSAR), require complex systems integration during vehicle development and do not support extending or upgrading embedded hardware and software after a vehicle is produced. This restriction, driven likely by safety concerns, is understandable for critical systems, such as braking and steering, power train, and driver assistance systems. However, extensibility of safety critical systems and software through features and apps produced by independent suppliers offers tremendous opportunities and is an important challenge that needs to be tackled. After a brief review of current automotive systems and software architectures and development methods, I will discuss the opportunities and challenges of upgradable cars, and sketch an extensible architecture and associated processes to support this vision.

26.11. 2013, 13:00, 0.2.90, Selma Lagerlöfs Vej 300
Nikolaj Bjorner, Microsoft Research, Redmond, USA
The Satisfiability Modulo Theories solver Z3

 Abstract: Automated reasoning has become an integral part of software engineering tools in recent years thanks to high-performance theorem provers. The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, Pex, Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Spec Explorer, SecGuru, and Terminator. These tools reduce program analysis, verification and testing problems to logic queries that are solved using Z3. The talk takes these applications of Z3 as a starting point and examines applications SAGE, Dafny and SecGuru in some more depth. SAGE uses dynamic symbolic execution. It has been used to eradicate hundreds of security vulnerabilities in media readers that are otherwise well-known to be prone to security critical bugs. Dafny is a program verification environment and presents the current state-of-the-art in program verification methodologies and tools. SecGuru is a tool for automatically validating network connectivity restriction policies in large scale data-centers such as Windows Azure. We then describe some of the current trends in Z3: including solving recursive Horn clauses, solving real and floating point arithmetic.

22.8. 2013, 14:00, 0.2.90, Selma Lagerlöfs Vej 300
Rasmus Ibsen-Jensen, Department of Computer Science, Aarhus University, Denmark
A faster algorithm for solving one-clock priced timed games

 Abstract: The talk will be an exposition of www.cs.au.dk/~reaper98/papers/priced.pdf. The talk will be about simple priced timed games, a subclass of one-clock priced timed games and build up to the definition of simple priced timed games using priced games - priced timed games without time. The main focus will be a specific example which the algorithm of the title will be used to solve. No prior knowledge about the area is expected.

22.8. 2013, 14:00, 0.2.90, Selma Lagerlöfs Vej 300
Hans Hüttel, Department of Computer Science, Aalborg University, Denmark
Types for resources in ψ-calculi

 Abstract: Several type systems have been proposed for capturing linear resource usage in variants of the pi-calculus. We use the general framework of pi-calculi by Bengtson et al. to establish a general type system that captures a diverse collection of type systems of this kind, including ones for liveness properties.

22.8. 2013, 14:00, 0.2.90, Selma Lagerlöfs Vej 300
Rasmus Ibsen-Jensen, Department of Computer Science, Aarhus University, Denmark
A faster algorithm for solving one-clock priced timed games

 Abstract: The talk will be an exposition of www.cs.au.dk/~reaper98/papers/priced.pdf. The talk will be about simple priced timed games, a subclass of one-clock priced timed games and build up to the definition of simple priced timed games using priced games - priced timed games without time. The main focus will be a specific example which the algorithm of the title will be used to solve. No prior knowledge about the area is expected.

14.8. 2013, 14:00, 0.2.90, Selma Lagerlöfs Vej 300
Dexter Kozen, Computer Science Department, Cornell University, USA
NetKAT: Foundations for Network Algebra

 Abstract: I will describe recent work on adapting Kleene Algebra with Tests (KAT) to reason about networks. NetKAT can be used to specify and verify network protocols and solve connectivity and optimization problems. There is a complete deductive system and PSPACE decision procedure.

14.3. 2013, 14:00, 0.2.90, Selma Lagerlöfs Vej 300
Giovanni Bacci, Department of Computer Science, Aalborg University, Denmark
On-the-Fly Exact Computation of Bisimilarity Distances

 Abstract: We propose an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented by Chen et. al. at FoSSaCS’12, proving that these distances can be computed in polynomial time using the ellipsoid method. Despite its theoretical importance, the ellipsoid method is known to be inefficient in practice. To overcome this problem, we propose an efficient on-the-fly algorithm which, unlike other existing solutions, computes exactly the distances between given states and avoids the exhaustive state space exploration. It is parametric in a given set of states for which we want to compute the distances. Our technique successively refines overapproximations of the target distances using a greedy strategy which ensures that the state space is further explored only when the current approximations are improved. Tests performed on a consistent set of (pseudo)randomly generated Markov chains shows that our algorithm improves, on average, the efficiency of the corresponding iterative algorithms with orders of magnitude.

28.2. 2013, 14:00, 0.2.13, Selma Lagerlöfs Vej 300
Omer Nguena-Timo, LaBRI, France
Runtime Enforcement of Timed Properties

 Abstract: Failure at runtime can be monitored and enforced by adding patches that control the outputs of the systems. In this talk we present two algorithms that allow to enforce real-time safety and co-safety properties. Properties are described with timed automata.

25.1. 2013, 14:00, 0.1.12, Selma Lagerlöfs Vej 300
Ramin Sadre, Department of Computer Science, Aalborg University, Denmark
Understanding Cloud Services on the Network Level

 Abstract: The advent of cloud services is changing the way computing power is delivered to enterprises and end users. Cloud services are very attractive in terms of costs, provisioning and scalability. This presentation addresses two upcoming challenges that cloud services will bring to network operators. First, it is to be expected that services such as cloud storage will soon generate a major portion of Internet traffic. Hence, it is essential to understand what workload such systems have to face and cause on the network. We present an empirical study of Dropbox. Second, outsourcing services to the cloud makes the customers extremely dependent on the cloud provider. This raises the question of whether the health of such services can still be monitored by the customers (or their Internet providers) without direct access to the servers. We evaluate how the health of remote services can be monitored solely by analyzing the network traffic exchanged between end users and cloud providers.

17.1. 2013, 13:00, 0.2.13, Selma Lagerlöfs Vej 300
Thomas Hildebrandt, Process and System Models Group, IT University of Copenhagen, Denmark
Live Sessions With Responses

 Abstract: We discuss ongoing work on sessions with responses as an extension of standard session types allowing to specify liveness properties. Concretely, sessions with responses are specified by annotating branching and selection labels with a finite conjunction of disjunctive responses. A disjunctive response is a finite disjunction of labels, and the intended meaning is that whenever a label is selected, one of the labels in each of the disjunctive responses is eventually selected. We illustrate the use of live sessions by a buyer/seller example where the buyer and seller engage in a potential infinite number of deals, and for each deal negotiates about the price but must eventually either agree or stop the negotiation. We informally describe a typing system for guaranteeing that well typed processes are live in this sense and discuss ongoing and future work.

17.10. 2012, 15:00, 0.2.90, Selma Lagerlöfs Vej 300
Simon Laursen, Department of Computer Science, Aalborg University, Denmark
Action Investment Energy Games

 Abstract: It is typical for an embedded system to have limited or constrained resources and to interact within an uncontrollable or even hostile environment. When adding this to the ever increasing demand on functionality and reliability for the lowest possible price, several interesting problems emerge. We introduce the formalism of action investment energy games where we study the trade-off between investments limited by given budgets and resource constrained (energy) behavior of the underlying system. More specifically, we consider energy games extended with costs of enabling actions and fixed budgets for each player. We ask the question whether for any Player 2 investment there exists a Player 1 investment such that Player 1 wins the resulting energy game. We study the action investment energy game for energy intervals with both upper and lower bounds, and with a lower bound only, and give a complexity results overview for the problem of deciding the winner in the game.

17.10. 2012, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Mathias Grund Sørensen, Department of Computer Science, Aalborg University, Denmark
Verification of Liveness Properties on Closed Timed-Arc Petri Nets

 Abstract: Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. In this talk, I will present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants, which uses optimized maximum constants for each place in the net to bound the size of the reachable state-space. We will also present experiments comparing the performance of this approach with the state-of-the-art model checker UPPAAL.

4.10. 2012, 15:00, 0.2.90, Selma Lagerlöfs Vej 300
John Lygeros, Automatic Control Laboratory, ETH Zurich, Switzerland
Introducing renewable generation into the power grid: What randomized optimization has to offer

 Abstract: Increasing concerns about energy security and sustainability have fueled a worldwide research effort into renewable energy sources. The introduction of renewable energy into the current power grid offers a wealth of challenges for control engineers, arising in energy production (e.g. optimization of wind turbines and wind farms), energy transmission and energy distribution (e.g. for distributed photovoltaic generation or demand response schemes). On the energy transmission level, a central concern is the uncertainty inherent in many forms of renewable generation, which is currently addressed through the procurement of reserves. In this talk we will discuss a stochastic programming problem to minimize the amount of reserves purchased subject to probabilistic constraints on meeting energy demand despite uncertainty in wind power in-feed. Motivated by the structure of the resulting optimization problem we develop a novel randomized optimization approach, which provides an interesting bridge between standard robust optimization and the scenario approach for chance constrained stochastic programs. The resulting method is tested in simulation on realistic scale power grids.

22.8. 2012, 14:30, 0.2.90, Selma Lagerlöfs Vej 300
Hao Wang, Center for Logic and Information, St Francis Xavier University, Canada
A Formal Diagrammatic Approach to Timed Workflow Modelling

 Abstract: A workflow model is an abstract representation of a real life workflow and consists of interconnected tasks depicting the desired executions of real life activities. Time information is an important aspect of many safety-critical workflows. This talk presents a new formal diagrammatic approach to timed workflow modelling involving principles from model-driven engineering. The approach extends the Diagram Predicate Framework, which is based on category theory and graph transformations, for the specification of workflow modelling formalisms. We develop a transition system to represent the dynamic semantics involving time in which transitions are described by specification transformations between instances. To model time, we introduce predicates for time delay and duration with transition rules for time advancement.

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