171 research outputs found
Bringing Model Checking Closer To Practical Software Engineering
Full text linkBal, H.E. [Promotor]Templon, J.A. [Copromotor]Willemse, T.A.C. [Copromotor
Analysis of Boolean Equation Systems through Structure Graphs
Full text linkWe analyse the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems with bisimilar structure graphs have the same solution. We show that our work conservatively extends earlier work, conducted by Keiren and Willemse, in which dependency graphs were used to analyse a subclass of Boolean equation systems, viz., equation systems in standard recursive form. We illustrate our approach by a small example, demonstrating the effect of simplifying an equation system through minimisation of its structure graph
Structural analysis of Boolean equation systems
No full textWe analyze the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems with bisimilar structure graphs have the same solution. We show that our work conservatively extends earlier work, conducted by Keiren and Willemse, in which dependency graphs were used to analyze a subclass of Boolean equation systems, viz., equation systems in standard recursive form. We illustrate our approach by a small example, demonstrating the effect of simplifying an equation system through minimization of its structure graph
Designing and describing QVTo model transformations
No full textModel transformations are the key technology of MDE that allows for software development using models as first-class artifacts. While there exist a number of languages that are specifically designed for programming model transformations, in practice, designing and maintaining model transformations still poses challenges. In this paper we demonstrate how mathematical notation of set theory and functions can be used for informal description and design of QVTo model transformations. We align the mathematical notation with the QVTo concepts, and use this notation to apply two design principles of developing QVTo transformations: structural decomposition and chain of model transformations
Equivalences for silent transitions in Probabilistic Systems (extended abstract)
Full text linkContains fulltext :
32472.pdf (Publisher’s version ) (Open Access
Verification using parameterised Boolean equation systems
No full textIn this note, we illustrate how parameterised Boolean equation systems can be employed for verifying system correctness. Several small examples are used to give a flavour of the more common techniques available for conducting typical verifications in this setting.We finish with a short discussion of the research challenges that lie ahead
The analysis of a conveyor belt system : a case study in hybrid systems and timed muCRL
Full text linkPrisoner's dilemma in software testing
Full text linkIn this article the problem of software testing is modeled as a formal strategic game. It is found that for certain values of the productivity and reward parameters the game is essentially equivalent to the Prisoner's Dilemma. This means that the game has a unique Nash equilibrium, which is not optimal for both players, however. Two formal games are described and analyzed in detaiJ, both capturing certain (though not all) aspects of real software testing procedures. Some of the literature on the Prisoner's Dilemma is reviewed and the r
- …
