| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Tree Regular Model Checking : A simulation-based approach
- 2006
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326 .- 1873-5940. ; 69:1-2, s. 93-121
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. In this framework, the central problem is to compute the transitive closure of a transducer. Such a representation allows to compute the set of reachable states of the system and to detect loops between states. A main obstacle of this approach is that there exists many systems for which the reachable set of states is not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states, which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation, which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to various protocols.
|
|
| 2. |
- Aziz Abdulla, Parosh, et al.
(författare)
-
Simulation-Based Iteration of Tree Transducers
- 2005
-
Ingår i: Proc. TACAS'05, 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
-
Konferensbidrag (refereegranskat)
|
|
| 3. |
- Kim, Jin-Hyun, et al.
(författare)
-
Optimizing the Resource Requirements of Hierarchical Scheduling Systems
- 2016
-
Ingår i: SIGBED Review. - : Association for Computing Machinery (ACM). - 1551-3688 .- 1551-3688. ; 13:3, s. 41-48
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- Compositional reasoning on hierarchical scheduling systems is a well-founded formal method that can construct schedulable and optimal system configurations in a compositional way. However, a compositional framework formulates the resource requirement of a component, called an interface, by assuming that a resource is always supplied by the parent components in the most pessimistic way. For this reason, the component interface demands more resources than the amount of resources that are really sufficient to satisfy sub-components. We provide two new supply bound functions which provides tighter bounds on the resource requirements of individual components. The tighter bounds are calculated by using more information about the scheduling system.We evaluate our new tighter bounds by using a model-based schedulability framework for hierarchical scheduling systems realized as Uppaal models. The timed models are checked using model checking tools Uppaal and Uppaal SMC, and we compare our results with the state of the art tool CARTS.
|
|
| 4. |
- Kunnappilly, Ashalatha, et al.
(författare)
-
Analyzing Ambient Assisted Living Solutions : A Research Perspective
- 2017
-
Ingår i: 12th International Conference on Design and Technology of Integrated Systems in Nanoscale Era DTIS 2017. - 9781509063772
-
Konferensbidrag (refereegranskat)abstract
- Typical AAL solutions rely on integrating capabilities for health monitoring, fall detection, communication and social inclusion, supervised physical exercises, vocal interfaces, robotic platforms etc. Ensuring the safe function and quality of service with respect to various extra-functional requirements like timing and security of such AAL solutions is of highest importance. To facilitate analysis, latest system development platforms provide underlying infrastructures for model-driven design (e.g., via the dime{} tool), timing and resource-usage specification (e.g., via the REMES tool), security features (e.g., by employing SECube), and statistical model-checking techniques (e.g, via Plasma). In this paper, we discuss the challenges associated with analyzing complex AAL solutions, from relevant properties to semantic interoperability issues raised by employing various frameworks for modeling and analysis, and applicability to evolving architectures. We take as examples two of the prominent existing AAL architectures and our own prior experience.
|
|
