807 research outputs found
Abstraction, prices and probability in model checking timed automata
No full textContains fulltext :
84322.pdf (Publisher’s version ) (Open Access)Radboud Universiteit Nijmegen, 03 november 2010Promotor : Vaandrager, F.W.178 p
Studies on verification of wireless sensor networks and abstraction learning for system inference
No full textContains fulltext :
93701.pdf (Publisher’s version ) (Open Access)Radboud Universiteit Nijmegen, 05 juli 2012Promotor : Vaandrager, F.W.140 p
Formal verification of on-chip communication fabrics
No full textContains fulltext :
103932.pdf (Publisher’s version ) (Open Access)Radboud Universiteit Nijmegen, 26 maart 2013Promotores : Vaandrager, F.W., Eekelen, M.C.J.D. van Co-promotor : Schmaltz, J.187 p
Performance analysis of real-time task systems using timed automata
No full textContains fulltext :
102351.pdf (Publisher’s version ) (Open Access)Radboud Universiteit Nijmegen, 22 januari 2013Promotor : Vaandrager, F.W.128 p
Supplementary material for publication "Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks"
No full textThis dataset contains supplementary material for the publication
F. Heidarian, J. Schmaltz and F.W. Vaandrager. Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. In Theoretical Computer Science 413:87-105, 2012. QAPL'10 special issue.
The following data are included:
1. A Uppaal model of the WSN protocol
2. A manual proof of correctness of the protocol
3. The sources of an Isabelle proof of correctness of the protoco
Active Model Learning for the Analysis of Network Protocols
No full textContains fulltext :
187331.pdf (Publisher’s version ) (Open Access)Radboud University, 13 april 2018Promotor : Vaandrager, F.W.xii, 172 p
Practical Automaton proofs in PVS
No full textContains fulltext :
32099_pracaupri.pdf (Publisher’s version ) (Open Access)This thesis is about an approach to modeling, validating and verifying com- puter-based systems. The kinds of systems we examine happen to be em- bedded systems, for the most part, but our approach is generally applicable to computer-based systems. Since veri?cation is essential to the production of safe and reliable systems, we feel the entire process that precedes the actual construction of such a system is in need of formal support; various studies in this thesis show how a systematic approach to modeling and val- idation can be applied to part of the software development lifecycle: the requirements and speci?cation phases. We focus on the practical side of modeling and validation, showing how to approach problems of ambiguity and incompleteness in the informal requirements. We illustrate some of the considerations used in arriving at the approach used in this thesis. The case studies and considerations show how this approach can be effective in ?nd- ing errors in models - errors which, when corrected, lead to better models and higher quality computer-based systems.RU Radboud Universiteit Nijmegen, 06 maart 2008Promotor : Vaandrager, F.W. Co-promotor : Hooman, J.J.M.285 p
Modeling and validating distributed embedded real-time control systems
No full textContains fulltext :
65551_modeanvad.pdf (Publisher’s version ) (Open Access)
Contains fulltext :
75289.pdf (Publisher’s version ) (Open Access)The development of complex embedded control systems can be improved significantly by applying formal techniques from control engineering and software engineering. It is shown how these approaches can be combined to improve the design and analysis of high-tech systems, both in theory and practice. The semantics of the integration of two established rigorous techniques has been defined formally in this work. The strength of this integrated semantics is demonstrated by means of a significant industrial case study: the embedded control of a printer paper path, whereby the full development life-cycle from model to realization is covered. The resulting model-driven design approach fits the current engineering practice in industry and is both flexible and effective.Radboud Universiteit Nijmegen, 21 januari 2009Promotor : Vaandrager, F.W. Co-promotor : Hooman, J.J.M.180 p
Compositional verification of hybrid systems using simulation relations
No full textContains fulltext :
32347.pdf (Publisher’s version ) (Open Access)The interaction of software with a physical environment can cause complex, mixed continuous-discrete behavior, also referred to as being hybrid. Formal verification can guarantee the conformance of the system with a specification on a design level. However, the computational cost limits its applicability to relatively simple systems. To enable the verification of larger hybrid systems, we extend two fundamental approaches from the discrete to the hybrid domain: abstraction and compositional reasoning. In an abstraction of a system, details of the behavior are neglected to decrease its complexity. To formally show abstraction we construct a simulation relation between the states of the models. A state simulates another if the same, or more, behavior is possible. A compositional analysis examines parts of the system in such a way that properties of the entire systems can be deduced, and simulation relations are well suited for this task. We extend the classic discrete simulation framework with an enhanced concept of simulation and additional proof rules for compositional reasoning. We show that this framework applies directly to hybrid systems that do not share variables by using well-known labeled transition system semantics. To deal with hybrid systems that share variables we propose a modified semantics that allows us to show compositionality for two fundamental classes of hybrid systems: those with unrestricted inputs, and hybrid automata with piecewise constant bounds on the derivatives and with convex linear constraints. Since any hybrid system can be approximated arbitrarily close with a decidable subset of the latter class, these results enable the algorithmic compositional verification of hybrid systems. Algorithms for checking simulation, compositional reasoning, and reachability analysis were implemented in a formally sound verification tool called PHAVer. It uses exact arithmetic and complexity management, and for some benchmarks outperforms even non-conservative, approximative, reachability tools.RU Radboud Universiteit Nijmegen, 10 oktober 2005Promotores : Vaandrager, F.W., Engell, S.VIII, 204 p
F.W. Angel memorial lecture ; 1970; F.W. Angel memorial lecture, 1970
No full textThe Third Annual F.W. Angel Memorial Lectur
- …
