| 1. |
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Algorithmic Improvements in Regular Model Checking
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by \em bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
|
|
| 3. |
- David, Alexandre, et al.
(författare)
-
A Formal Semantics for UML Statecharts
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The UML language is a large set of notations and rules to describe different aspects of a system. It provides a set of diagrams to view the system from different angles: use case diagrams, class diagrams, statecharts diagrams, and deployment diagrams are some of them. In this report we are interested in the statecharts diagrams that describe dynamic behaviours. We give a formal semantics for a large subset of these statecharts, in particular we focus on the action language semantics. Our subset and semantics are very close to the one supported by the tool Rhapsody.
|
|
| 4. |
- d'Orso, Julien, 1975-
(författare)
-
New Directions in Symbolic Model Checking
- 2003
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- In today's computer engineering, requirements for generally high reliability have pushed the notion of testing to its limits. Many disciplines are moving, or have already moved, to more formal methods to ensure correctness. This is done by comparing the behavior of the system as it is implemented against a set of requirements. The ultimate goal is to create methods and tools that are able to perform this kind of verfication automatically: this is called Model Checking. Although the notion of model checking has existed for two decades, adoption by the industry has been hampered by its poor applicability to complex systems. During the 90's, researchers have introduced an approach to cope with large (even infinite) state spaces: Symbolic Model Checking. The key notion is to represent large (possibly infinite) sets of states by a small formula (as opposed to enumerating all members). In this thesis, we investigate applying symbolic methods to different types of systems: Parameterized systems. We work whithin the framework of Regular Model Chacking. In regular model checking, we represent a global state as a word over a finite alphabet. A transition relation is represented by a regular length-preserving transducer. An important operation is the so-called transitive closure, which characterizes composing a transition relation with itself an arbitrary number of times. Since completeness cannot be achieved, we propose methods of computing closures that work as often as possible. Games on infinite structures. Infinite-state systems for which the transition relation is monotonic with respect to a well quasi-ordering on states can be analyzed. We lift the framework of well quasi-ordered domains toward games. We show that monotonic games are in general undecidable. We identify a subclass of monotonic games: downward-closed games. We propose an algorithm to analyze such games with a winning condition expressed as a safety property. Probabilistic systems. We present a framework for the quantitative analysis of probabilistic systems with an infinite state-space: given an initial state sinit, a set F of final states, and a rational Θ > 0, compute a rational ρ such that the probability of reaching F form sinit is between ρ and ρ + Θ. We present a generic algorithm and sufficient conditions for termination.
|
|
| 5. |
- Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d'Orso.
(författare)
-
Deciding Monotonic Games.
- 2003
-
Ingår i: CSL/KGC'03, Computer Science Logic and 8th Kurt Gödel Colloquium.
-
Konferensbidrag (refereegranskat)
|
|
