Fundamenta Informaticae - Volume 93, issue 1-3

Authors: Niewiadomski, Artur | Penczek, Wojciech | Szreter, Maciej

Article Type: Research Article

Abstract: The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the …(prototype) tool BMC4UML and some experimental results are presented. Show more

Keywords: UML, Bounded Model Checking, symbolic verification

DOI: 10.3233/FI-2009-0103

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 289-303, 2009

Authors: Rataj, Artur | Woźna, Bożena | Zbrzezny, Andrzej

Article Type: Research Article

Abstract: The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be build. Therefore, we have developed the J2TADD tool that translates a Java program to a network of TADDs; the paper presents this tool. The J2TADD tool works in two stages. The first one consists …in translation of a Java code to an internal assembly language (IAL). Then, the resulting assembly code is translated to a network of TADDs. We exemplify the use of the translator by means of the following well-known concurrency examples written in Java: race condition problem, dining philosophers problem, single sleeping barber problem and readers and writers problem. Show more

DOI: 10.3233/FI-2009-0104

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 305-324, 2009

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: The paper is an attempt to see how much we can learn about a given Parsing Expression Grammar with the help of classical concepts used in the construction of predictive top-down parsers.

DOI: 10.3233/FI-2009-0105

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 325-336, 2009

Authors: Wegener, Jan-Thierry | Popova-Zeugmann, Louchka

Article Type: Research Article

Abstract: We present Petri nets with time windows (tw-PN) where each place is associated with an interval (window). Every token which arrives at a place gets a real-valued clock which shows its "age". A transition can fire when all needed tokens are "old enough". When a token reaches an "age" equal to the upper bound of the place where it is situated, the "token's age", i.e., clock will be reset to zero. Following …this we compare these time dependent Petri nets with their (timeless) skeletons. The sets of both their reachable markings are equal, their liveness behaviour is different, and neither is equivalent to Turing machines. We also prove the existence of runs where time gaps are possible in the tw-PN, which is an extraordinary feature. Show more

DOI: 10.3233/FI-2009-0106

Citation: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 337-352, 2009