General

2010

Joost-Pieter Katoen, Advances in Probabilistic Model Checking, in: Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 25, Springer-Verlag, 2010    

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns and Joost-Pieter Katoen, Performance Evaluation and Model Checking Join Forces (2010), in: Communications of the ACM       

2008

Joost-Pieter Katoen, Perspectives in Probabilistic Verification, in: 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 3-10, IEEE CS Press, 2008        

Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008   

 

WP1: Modelling and Specification

2011

Uli Fahrenberg, Line Juhl, Kim G. Larsen and Jiri Srba, Energy Games in Multiweighted Automata, 2011           

J. Berendsen, B. Gebremichael, Frits Vaandrager and M. Zhang, Formal Specification and Analysis of Zeroconf using Uppaal (2011), in: ACM Transactions on Embedded Computing Systems, 10:3       

F. Houben, G. Igna and Frits Vaandrager, Modeling Task Systems Using Parameterized Partial Orders, 2011    

Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter and Lijun Zhang, Probabilistic Logical Characterization (2011), in: Information and Computation, 209:2(154-172)            

Bernoit Caillaud, Constraint Markov Chains -- full version (2011), in: Theoretical Computer Science

2010

Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga and Mark Timmer, A Linear Process Algebraic Format for Probabilistic Systems with Data, in: Applications of Concurrency to System Design (ACSD), IEEE CS Press, 2010            

Joost-Pieter Katoen, J. van de Pol, Marielle Stoelinga and Mark Timmer, A linear process-algebraic format for probabilistic systems with data (extended version), University of Twente, number TR-CTIT-10-11, 2010

Christian Eisentraut, Holger Hermanns and Lijun Zhang, Concurrency and Composition in a Stochastic World, in: CONCUR 2010, pages 21-39, Springer, 2010

P. Ganty, G. Geeraerts, Jean-François Raskin and Laurent Van Begin, Le problème de couverture pour les réseaux de Petri. Résultats classiques et développements récents (2010), in: Techniques et Sciences Informatiques, 28:9(1107-1142)        

T. Basten, Benthum E. van, M. Geilen, M. Hendriks, F. Houben, G. Igna, F. Reckers, Smet S. de, L. Somers, E. Teeselink, N. Trcka, Frits Vaandrager, J. Verriet, M. Voorhoeve and Y. Yang, Model-Driven Design-Space Exploration for Embedded Systems: The Octopus Toolset, in: Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I, pages 90-105, Springer, 2010

Christian Eisentraut, Holger Hermanns and Lijun Zhang, On Probabilistic Automata in Continuous Time, in: LICS, pages 342-351, IEEE Computer Society, 2010

Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun, Pebble weighted automata and transitive closure logics, in: Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10)—Part II, pages 587-598, Springer, 2010

Holger Hermanns and Joost-Pieter Katoen, The How and Why of Interactive Markov Chains, in: Formal Methods for Components and Objects (FMCO), pages 311-337, Springer-Verlag, 2010      

D. K. Kaynar, N. A. Lynch, R. Segala and Frits Vaandrager, The Theory of Timed I/O Automata (second edition), Morgan & Claypool Publishers, 2010

Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen and Saulius Pusinskas, Scenario-Based Analysis and Synthesis of Real-Time Systems Using Uppaal, in: Proc. 13th Conf. on Design, Automation and Test in Europe (DATE'10), pages "", IEEE, 2010

2009

Hichem Boudali, Pepijn Crouzen and Marielle Stoelinga, A Rigorous, Compositional, and Extensible Framework for Dynamic Fault Tree Analysis (2009), in: IEEE Trans. Dependable Sec. Comput., 7:2(128-143)

Hichem Boudali, Marielle Stoelinga and Hasan Sozer, Architectural Availability Analysis of Software Decomposition for Local Recovery, in: Proceedings of the Third IEEE International Conference on Secure Software Integration and Reliability Improvement, Los Alamitos, pages 14-22, IEEE Computer Society, 2009

Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen and Thomas Noll, Codesign of Dependable Systems: A Component-Based Modeling Language, in: Proc. 7th ACM-IEEE Int. Conf. on Formal Methods and Models for Codesign (MEMOCODE 2009), pages 121-130, IEEE CS Press, 2009

Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakov, Ralf Wimmer and Bernd Becker, Compositional Dependability Evaluation for STATEMATE (2009), in: IEEE Transaction on Software Engineering, 35:2(274-292).

Marielle Stoelinga, Compositional dependability modeling using Arcade, in: Proceedings of the 9th Workshop on Specification and Verification of Component-based systems, 2009            

Patricia Bouyer and Antoine Petit, On extensions of timed automata, in: Perspectives in Concurrency Theory, pages 35-63, Universities Press, 2009          

Holger Hermanns and Joost-Pieter Katoen, The How and Why of Interactive Markov Chains, pages 311-337, Springer, 2009           

Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen and Saulius Pusinskas, Verifying Real-Time Systems against Scenario-Based Requirements, in: Proc. 16th International Symposium on Formal Methods (FM'09), pages 676-691, Springer, 2009   

Benedikt Bollig and Paul Gastin, Weighted versus Probabilistic Logics, in: Proceedings of the 13th International Conference on Developments in Language Theory (DLT'09), pages 18-38, Springer, 2009          

 

2008

Claus Thrane, Ulrich Fahrenberg and Kim G. Larsen, : Quantitative simulations of weighted transition systems, in: Proceedings of Nordic Workshop on Programming Theory, 2008   

Hichem Boudali, Pepijn Crouzen, Boudewijn R. Haverkort, Matthias Kuntz and Marielle Stoelinga, Architectural dependability evaluation with Arcade, in: The 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2008, June 24-27, 2008, Anchorage, Alaska, USA, Proceedings, pages 512-521, IEEE Computer Society, 2008

Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre, Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains, in: Hybrid Systems: Computation and Control (HSCC), pages 244-258, Springer Verlag, 2008   

Ulrich Fahrenberg and Kim G. Larsen, Discount-Optimal Infinite Runs in Priced Timed Automata., in: Proceedings of INFINITY 2008 10th International Workshop on Verification of Infinite-State Systems, 2008     

Patricia Bouyer, Ulrich Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiri Srba, Infinite Runs in Weighted Timed Automata with Energy Constraints, in: 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08), Saint-Malo, France, pages 33-47, Springer, 2008           

Patricia Bouyer, Kim G. Larsen and Nicolas Markey, Model Checking One-clock Priced Timed Automata (2008), in: LMCS, 4:2:9            

Patricia Bouyer, Nicolas Markey, Joel Ouaknine and James Worrell, On Expressiveness and Complexity in Real-time Model Checking, in: ICALP'08, Reykjavik, Iceland, pages 124-135, Springer, 2008     

Pepijn Crouzen, Holger Hermanns and Lijun Zhang, On the Minimisation of Acyclic Models, in: CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, pages 295-309, Springer, 2008           

Kim G. Larsen and Jacob I. Rasmussen, Optimal reachability for multi-priced timed automata. (2008), in: Theoretical Computer Science, 390:2-3(197-213)    

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Nicolas Markey, Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, in: QEST'08, Saint-Malo, France, pages 55-64, IEEE Computer Society Press, 2008           

Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen and Martin Leucker, Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning, in: 19th International Conference on Concurrency Theory (CONCUR'08), pages 162-166, Springer, 2008         

Joost-Pieter Katoen, M Bozzanol, G Burte, A Cimatti, M. le Coroller, Viet Yen Nguyen, T Noll and X Olive, System and Software Co-Engineering: Performance and Verification, in: ESA ADCCS Workshop, Noordwijk, The Netherlands, 2008      

Mani Swaminathan, Martin Fraenzle and Joost-Pieter Katoen, The Surprising Robustness of (Closed) Timed Automata against Clock-Drift, in: 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2008   

Taolue Chen, Tingting Han and Joost-Pieter Katoen, Time-Abstracting Bisimulation for Probabilistic Timed Automata, in: 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 177-184, IEEE CS Press, 2008

Publications for topic: WP2: Analysis

2011

Joost-Pieter Katoen, J. van de Pol, Marielle Stoelinga and Mark Timmer, A linear process-algebraic format with data for probabilistic automata (2011), in: Theoretical Computer Science

Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher and Andrzej Wasowski, Abstract Probabilistic Automata, in: Verification, Model Checking and Abstract Interpretation (VMCAI), pages 324-339, Springer-Verlag, 2011          

Benoit Delahaye, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen and Andrzej Wasowski, APAC: a tool for reasoning about Abstract Probabilistic Automata, 2011        

Mark Timmer, Marielle Stoelinga and J. van de Pol, Confluence Reduction for Probabilistic Systems, in: Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 311-325, Springer Verlag, 2011      

Radu Mardare, Luca Cardelli and Kim G. Larsen, Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas, 2011

Benoit Delahaye, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen and Andrzej Wasowski, Decision Problems for Interval Markov Chains, 2011

Uli Fahrenberg, Claus Thrane and Kim G. Larsen, Distances for Weighted Transition Systems: Games and Properties, 2011         

Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre, Efficient CTMC Model Checking of Linear Real-Time Objectives, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 128-142, 2011        

Uli Fahrenberg, Line Juhl, Kim G. Larsen and Jiri Srba, Energy Games in Multiweighted Automata, 2011           

Sebastian S. Bauer, Line Juhl, Kim G. Larsen, Axel Legay and Jiri Srba, Extending Modal Transition Systems with Structured Labels, 2011         

Paolo Ballarini, Hilal Djafri, Marie Duflot, Serge Haddad and Nihal Pekergin, HASL: An Expressive Language for Statistical Verification of Stochastic Models, in: Proceedings of the 5th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'11), 2011      

Martin Fraenzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick and Lijun Zhang, Measurability and Safety Verification for Stochastic Hybrid Systems, in: Proceedings of the 14th international conference on Hybrid systems: computation and control, pages 43-52, ACM, 2011  

Uli Fahrenberg, Kim G. Larsen and Claus Thrane, Metrics for Weighted Transition Systems: Axiomatization and Complexity (2011), in: Theoretical Computer Science

Pierre-Alain Reynier Reynier and Frédéric Servais, Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning, in: Proc. 32nd International Conference on Application and Theory of Petri Nets (PETRI NETS 2011), Springer, 2011

Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang, Model Checking Algorithms for CTMDPs, in: 23rd Int. Conf. on Computer Aided Verification (CAV 2011), Springer, 2011     

Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre, Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications (2011), in: Logical Methods in Computer Science, 7:1-2(1-34)      

Radu Mardare, Luca Cardelli and Kim G. Larsen, Modular Markovian Logic, 2011            

Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen, F. Sher and Andrzej Wasowski, New Results on Abstract Probabilistic Automata, 2011

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski, Timothy Bourke and Didier Lime, New Results on Timed Specifications, 2011

T Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, Jean-François Raskin and J. Worrell, On reachability for Hybrid Automata over Bounded Time, in: ICALP'11, Springer, 2011          

Holger Hermanns, Arnd Hartmanns, Jonathan Bogdoll and Luis María Ferrer Fioriti, Partial Order Methods for Statistical Model Checking and Simulation, in: Proc. 13th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems and 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FMOODS/FORTE), 2011     

Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang, Probabilistic reachability for parametric Markov models (2011), in: International Journal on Software Tools for Technology Transfer, 13:1(3-19)    

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen and Nicolas Markey, Quantitative analysis of real-time systems using priced timed automata (2011), in: Communications of the ACM

Sebastian Bauer, Uli Fahrenberg, Line Juhl, Kim G. Larsen, Axel Legay and Claus Thrane, Quantitative Refinement for Weighted Modal Transition Systems, 2011

Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst Moritz Hahn, Safety Verification for Probabilistic Hybrid Systems (2011), in: European Journal of Control

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny B. Poulsen, Jonas V. Vliet and Zheng Wang, Statistical Model Checking for Networks of Priced Timed Automata, 2011

Ernst Moritz Hahn, Tingting Han and Lijun Zhang, Synthesis for PCTL in Parametric Markov Decision Processes, in: NASA Formal Methods, pages 146-161, Springer, 2011

Joost-Pieter Katoen, Daniel Klink, Martin Leucker and Verena Wolf, Three-Valued Abstraction for Probabilistic Systems (2011), in: Journal on Logic and Algebraic Programming(1-55)    

Alexandre David, Axel Legay, Zheng Wang, Kim G. Larsen and Marius Mikucionis, Time for Statistical Model Checking of Real-time Systems, in: Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV),Springer Verlag, 2011     

Daniel Klink, Anne Remke, Boudewijn R. Haverkort and Joost-Pieter Katoen, Time-Bounded Reachability in Tree-Structured QBDs by Abstraction (2011), in: Performance Evaluation, 68:2(105-125)        

Patricia Bouyer, Franck Cassez and François Laroussinie, Timed Modal Logics for Real-Time Systems: Specification, Verification and Control (2011), in: Journal of Logic, Language and Information, 20:2(169-203)     

2010

Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga and Mark Timmer, A Linear Process Algebraic Format for Probabilistic Systems with Data, in: Applications of Concurrency to System Design (ACSD), IEEE CS Press, 2010

Joost-Pieter Katoen, J. van de Pol, Marielle Stoelinga and Mark Timmer, A linear process-algebraic format for probabilistic systems with data (extended version), University of Twente, number TR-CTIT-10-11, 2010

Uli Fahrenberg, Kim G. Larsen and Cluas Thrane, A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic (2010), in: Computing and Informatics:29   

J. Berendsen, Abstraction, Prices and Probability in Model Checking Timed Automata, Radboud University Nijmegen, 2010          

Joost-Pieter Katoen, Advances in Probabilistic Model Checking, in: Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 25, Springer-Verlag, 2010

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman and Andrzej Wasowski, ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems, in: Proceedings of Automated Technology for Verification and Analysis, pages 365-370, Springer, 2010

Alessandro Abate, Joost-Pieter Katoen, John Lygeros and Maria Prandini, Approximate model checking of stochastic hybrid systems (2010), in: European Journal of Control, 16:6(624-641)             

Mark Timmer, Marielle Stoelinga and J. van de Pol, Confluence Reduction for Probabilistic Systems (extended version), ArXiv e-prints, number 1011.2314, Technical Report, 2010          

Erika Abraham, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen and Bernd Becker, DTMC Model Checking by SCC Reduction, in: 7th Int. Conf. on Quantitative Evaluation of Systems (QEST'10), Williamsburg, VA, USA, pages 37-46, IEEE CS Press, 2010

Pierre Ganty, Nicolas Maquet and Jean-François Raskin, Fixed point guided abstraction refinement for alternating automata (2010), in: Theor. Comput. Sci., 411(3444-3459)

J. Berendsen, David N. Jansen and Frits Vaandrager, Fortuna: Model Checking Priced Probabilistic Timed Automata, in: QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Viginia, USA, 15-18 September 2010, pages 273-281, IEEE Computer Society, 2010        

G. Geeraerts, G. Kalyon, T. Le Gall, N. Maquet and Jean-François Raskin, Lattice-Valued Binary Decision Diagrams, in: Proceedings of ATVA 2010, 8th international symposium on Automated Technology for Verification and Analysis, pages 158-172, 2010   

Lijun Zhang and Martin R. Neuhäußer, Model Checking Interactive Markov Chains, in: Sixteenth International Conference on tools and algorithms for the construction and analysis of systems (TACAS), Springer, 2010

Lijun Zhang and Martin R. Neuhäußer, Model Checking Interactive Markov Chains, in: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 53-68, Springer, 2010            

Andreas Classens, Patrick Heymans, Axel Legay, Jean-François Raskin and Pierre-Yves Schobbens, Model Checking lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines (2010), in: ICSE'2010 - IEEE

Falko Dulat, Joost-Pieter Katoen and Viet Yen Nguyen, Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report, in: Proceedings of 7th European Performance Engineering Workshop (EPEW 2010), Springer, 2010            

S. Akshay, Paul Gastin, Madhavan Mukund and K. Narayan Kumar, Model checking time-constrained scenario-based specifications, in: Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), pages 204-215, Leibniz-Zentrum für Informatik, 2010        

Gilles Geeraerts, Jean-François Raskin and Laurent Van Begin, On the efficient computation of the coverability set of Petri nets (2010), in: International Journal of Foundations of Computer Science, 21:2(135-165)           

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, PARAM: A Model Checker for Parametric Markov Models, in: Computer Aided Verification, pages 660-664, Springer Berlin / Heidelberg, 2010       

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, PASS: Abstraction Refinement for Infinite Probabilistic Models, in: TACAS, 2010          

Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun, Pebble weighted automata and transitive closure logics, in: Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10)~-- Part~II, pages 587-598, Springer, 2010         

Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns and Joost-Pieter Katoen, Performability Assessment by Model Checking of Markov Reward Models (2010), in: Formal Methods in Systems Design, 36:1(1-36)      

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns and Joost-Pieter Katoen, Performance Evaluation and Model Checking Join Forces (2010), in: Communications of the ACM, 53:9(76-85)          

Uli Fahrenberg, Kim G. Larsen and Claus Thrane, Quantitative Analysis of Weighted Transition Systems (2010), in: Logic and Algebraic Programming -- Special Issue of NWPT08      

Claus R. Thrane, Uli Fahrenberg and Kim G. Larsen, Quantitative analysis of weighted transition systems (2010), in: J. Log. Algebr. Program., 79:7(689-703)

Qi Lu, Michael Madsen, Maritn Milata and Søren Ravn, Uli Fahrenberg and Kim G. Larsen, Reachability Analysis for Timed Automata using Max-Plus Algebra, 2010

Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst Moritz Hahn, Safety Verification for Probabilistic Hybrid Systems, in: Computer Aided Verificatio, pages 196-211, Springer, 2010      

Shuhao Li, Sandie Balaguer, Alexandre David, Kim G. Larsen, Brian Nielsen and Saulius Pusinskas, Scenario-based verification of real-time systems using Uppaal (2010), in: Formal Methods in System Design, 37:2-3(200-264)            

Holger Hermanns and Joost-Pieter Katoen, The How and Why of Interactive Markov Chains, in: Formal Methods for Components and Objects (FMCO), pages 311-337, Springer-Verlag, 2010      

D. K. Kaynar, N. A. Lynch, R. Segala and Frits Vaandrager, The Theory of Timed I/O Automata (second edition), Morgan & Claypool Publishers, 2010            

Georgel Calin, Pepijn Crouzen, Pedro D'Argenio, Ernst Moritz Hahn and Lijun Zhang, Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains, in: SPIN, pages 193-211, Springer, 2010           

Martin R. Neuhäußer and Lijun Zhang, Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes, in: Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2010         

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen and Nicolas Markey, Timed Automata with Observers under Energy Constraints, in: Proceedings of the 13th International Conference on Hybrid Systems: Computation and Control (HSCC'10), ACM Press, 2010          

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman and Andrzej Wasowski, Timed I/O Automata: A Complete Specification Theory for Real-time Systems, in: Proceedings of Hybrid Systems: Computation and Control, ACM, 2010   

Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey and Ghassan Oreiby, Using Model Checking for Analyzing Distributed Power Control Problems (2010), in: EURASIP Journal on Wireless Communications and Networking, 2010:861472

2009

Uli Fahrenberg, Kim G. Larsen and Claus Thrane, A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic, in: Doctoral Workshop on Mathematical and Engineering in Computer Science, 2009   

Reza Pulungan and Holger Hermanns, Acyclic Minimality by Construction---Almost, in: Fifth International Conference on the Quantitative Evaluation of Systems (QEST 2009), 13-16 September, 2009, Budapest, Hungary, IEEE Computer Society, 2009

Hichem Boudali, Marielle Stoelinga and Hasan Sozer, Architectural Availability Analysis of Software Decomposition for Local Recovery, in: Proceedings of the Third IEEE International Conference on Secure Software Integration and Reliability Improvement, Los Alamitos, pages 14-22, IEEE Computer Society, 2009         

Peter Bulychev, Thomas Chatain, Alexandre David and Kim G. Larsen, Checking simulation relation between timed game automata, in: Proceedings of the 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), pages 73-87, Springer, 2009      

Véronique Bruyère, Jean-François Raskin and Emmanuel D'allolio, Durations and Parametric Model-Checking in Timed Automata (2009), in: Transactions on Computational Logic, 9:2(1-20)         

Pierre Ganty, Nicolas Maquet and Jean-François Raskin, Fixpoint Guided Abstraction for Alternating Automata (2009), in: CIAA'09 - LNCS, 5642(155-164)

Laurent Doyen and Jean-François Raskin, Improved Algorithms for the Automata-Based Approach to Model-Checking (2009), in: Logical Methods in Computer Science, 5:1:5  

Pierre Ganty, Gilles Geeraerts, Jean-François Raskin and Laurent Van Begin, Méthodes algorithmiques pour l'analyse des réseaux de Petri (2009), in: Techniques et Sciences Informatiques   

Pierre Ganty, Jean-François Raskin and Laurent Van Begin, On the efficient computation of the coverability set for Petri nets (2009), in: International Journal of Foundations of Computer Science    

Nikola Benes, Jan Kret'inský, Kim Guldstrand Larsen and Jiri Srba, Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete, in: ICTAC, pages 112-126, 2009

Joost-Pieter Katoen, Daniel Klink and Martin R. Neuhäußer, Compositional Abstraction of Stochastic Systems, in: Formal Modeling and Analysis of Timed Systems (FORMATS), pages 195-211, Springer, 2009  

Benoit Caillaud, Benoit Delahaye, Kim G. Larsen, Mikkel Larsen Pedersen and Andrzej Wasowski, Compositional Design Methodology with Constraint Markov Chains, 2009

Tingting Han, Joost-Pieter Katoen and Berteun Damman, Counterexample Generation in Probabilistic Model Checking (2009), in: IEEE Transactions on Software Engineering, 35:2(241-257)

Martin R. Neuhäußer, Marielle Stoelinga and Joost-Pieter Katoen, Delayed Nondeterminism in Continuous-Time Markov Decision Processes, in: Foundations of Software Science and Computation Structures (FoSSaCS), pages 364-379, Springer-Verlag, 2009        

Tingting Han, Diagnosis, Synthesis and Analysis of Probabilistic Models, University of Twente and RWTH Aachen University, 2009         

Ulrich Fahrenberg and Kim Guldstrand Larsen, Discount-Optimal Infinite Runs in Priced Timed Automata (2009), in: Electr. Notes Theor. Comput. Sci., 239(179-191)       

Ulrich Fahrenberg and Kim Guldstrand Larsen, Discounting in Time (2009), in: Electr. Notes Theor. Comput. Sci., 253:3(25-31)    

Alexandre David, Kim G. Larsen, Thomas Chatain and and Peter Bulychev, Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation., in: In Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems, pages 73-87, 2009            

Adam Antonik, Michael Huth, Kim Guldstrand Larsen, Ulrik Nyman and Andrzej Wasowski, EXPTIME-complete Decision Problems for Modal and Mixed Specifications (2009), in: Electr. Notes Theor. Comput. Sci., 242:1(19-33)            

J. Berendsen, D. N. Jansen and F. W. Vaandrager, Fortuna: Model Checking Priced Probabilistic Timed Automata, Institute for Computing and Information Sciences, Radboud University Nijmegen, Report, 2009  

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, INFAMY: An Infinite-State Markov Model Checker, in: CAV, pages 641-647, Springer Verlag, 2009

Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre, LTL model checking of time-inhomogeneous Markov chains, in: 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), pages 104-119, 2009    

Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp and Joost-Pieter Katoen, Maximizing System Lifetime by Battery Scheduling, in: 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, IEEE Computer Society, 2009     

Patricia Bouyer, Model-Checking Timed Temporal Logics, in: Proceedings of the 4th Workshop on Methods for Modalities (M4M-5), pages 323-341, Elsevier Science Publishers, 2009     

Thomas Chatain, Alexandre David and Kim G. Larsen, Playing Games with Timed Games, in: Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS'09), 2009         

Alexandre David, Kim G. Larsen and Thomas Chatain, Playing Games with Timed Games, in: In proceedings of 3rd IFAC Conference on analysis and Design of Hybrid Systems, 2009           

Kim G. Larsen, Priced Timed Automata: Theory and Tools, in: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009), pages 417-425, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009          

Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang, Probabilistic Reachability for Parametric Markov Models, in: SPIN, Grenoble, France, pages 88-106, Springer, 2009      

Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre, Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications, in: IEEE Symposium on Logic in Computer Science (LICS), IEEE CS Press, 2009    

Patricia Bouyer and Vojtv ech Forejt, Reachability in Stochastic Timed Games, in: Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP'09), pages 103-114, Springer, 2009            

Bastian Schlich, Thomas Noll, Jörg Brauer and Lucas Brutschy, Reduction of Interrupt Handler Executions for Model Checking Embedded Software, in: Proc. of Haifa Verification Conference 2009 (HVC 2009), Springer, 2009            

Joost-Pieter Katoen and Ivan S. Zapreev, Simulation-based CTMC Model Checking: An Empirical Evaluation, in: Quantitative Evaluation of Systems (QEST), pages 31-40, IEEE CS Press, 200   

J. Berendsen, D. N. Jansen, J. Schmaltz and F. W. Vaandrager, The Axiomatization of Override and Update (2009), in: Journal of Applied Logic   

Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns and David N. Jansen, The Ins and Outs of The Probabilistic Model Checker MRMC, in: Quantitative Evaluation of Systems (QEST), Budapest, Hungary, pages 167-176, IEEE Computer Society, 2009        

TIME 2009, 16th International Symposium on Temporal Representation and Reasoning, Bressanone-Brixen, Italy, 23-25 July 2009, Proceedings, IEEE Computer Society, 2009

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains (2009), in: Fundamenta Informaticae, 95(129-155)            

Daniel Klink, Anne Remke, Boudewijn R. Haverkort and Joost-Pieter Katoen, Time-Bounded Reachability in Tree-Structured QBDs by Abstraction, in: Quantitative Evaluation of Systems (QEST), pages 133-142, IEEE CS Press, 2009   

J. Berendsen, T. Chen and D. N. Jansen, Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata, in: Theory and Applications of Models of Computation, 6th Annual Conference, TAMC 2009, Changsha, China, May 18-22, 2009. Proceedings, pages 128-137, Springer, 2009        

Patricia Bouyer, Thomas Brihaye and Fabrice Chevalier, Weighted O-Minimal Hybrid Systems (2009), in: Annals of Pure and Applied Logics, 161:3(268-288)     

Benedikt Bollig and Paul Gastin, Weighted versus Probabilistic Logics, in: Proceedings of the 13th International Conference on Developments in Language Theory (DLT'09), pages 18-38, Springer, 2009          

2008

Lijun Zhang, A Space-Efficient Probabilistic Simulation Algorithm, in: Concurrency Theory (CONCUR), pages 248-263, Springer, 2008   

Joost-Pieter Katoen, Daniel Klink, Martin Leucker and Verena Wolf, Abstraction for Stochastic Systems by Erlang's Method of Stages, in: 19th International Conference on Concurrency Theory (CONCUR'08), pages 279-294, Springer, 2008           

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Größer, Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata, in: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), pages 217-226, IEEE Computer Society Press, 2008       

Thomas Noll and Bastian Schlich, Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code, in: Hardware and Software: Verification and Testing (Haifa Verification Conference, HVC), pages 185-201, Springer, 2008           

Ulrich Fahrenberg and Kim G. Larsen, Discount-Optimal Infinite Runs in Priced Timed Automata., in: Proceedings of INFINITY 2008 10th International Workshop on Verification of Infinite-State Systems, 2008     

Reza Pulungan and Holger Hermanns, Effective Minimization of Acyclic Phase-Type Representations, in: Analytical and Stochastic Modeling Techniques and Applications, 15th International Conference, ASMTA 2008, Nicosia, Cyprus, June 4-6, 2008, Proceedings, Nicosia, Cyprus, pages 128-143, Springer, 2008  

Sebastian Kupferschmid, Jörg Hoffmann and Kim G. Larsen, Fast Directed Model Checking Via Russian Doll Abstraction., in: Proceedings of TACAS 2008, 2008            

Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand and David N. Jansen, Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations (2008), in: Special Issue on TACAS 2007, Logical Method in Computer Science (LMCS)        

Joost-Pieter Katoen and Alexandru Mereacre, Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains, in: FORMATS'08, Springer-Verlag, 2008   

Patricia Bouyer, Kim G. Larsen and Nicolas Markey, Model Checking One-clock Priced Timed Automata (2008), in: LMCS, 4:2:9            

Marcin Jurdzi'nski, François Laroussinie and Jeremy Sproston, Model Checking Probabilistic Timed Automata with One or Two Clocks (2008), in: Logical Methods in Computer Science, 4:3

Kim G. Larsen and Jacob I. Rasmussen, Optimal reachability for multi-priced timed automata. (2008), in: Theoretical Computer Science, 390:2-3(197-213)    

Alexandre David, Piotr Kordy, Kim G. Larsen and Jan Willen Polderman, Practical Robustness Analysis of Timed Automata, 2008         

Holger Hermanns, Björn Wachter and Lijun Zhang, Probabilistic CEGAR, in: 20th International Conference on Computer Aided Verification (CAV), pages 162-175, Springer, 2008          

Gerlind Herberich, Thomas Noll, Bastian Schlich and Carsten Weise, Proving Correctness of an Efficient Abstraction for Interrupt Handling, in: Proceedings 3rd International Workshop on Systems Software Verification (SSV), pages 133-150, Elsevier, 2008          

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Nicolas Markey, Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, in: QEST'08, Saint-Malo, France, pages 55-64, IEEE Computer Society Press, 2008           

Berteun Damman, Tingting Han and Joost-Pieter Katoen, Regular Expressions for PCTL Counterexamples, in: Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2008

Reza Pulungan and Holger Hermanns, The Minimal Representation of the Maximum of Erlang Distributions, in: Proceedings 14th GI/ITG Conference on Measurement, Modelling and Evaluation of Computer and Communication Systems (MMB 2008), March 31 - April 2, 2008, Dortmund, Germany, GI Fachausschuss 3.2 / ITG Fachausschuss 6.5, Dortmund, Germany, pages 207-222, VDE Verlag, 2008           

Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn and Björn Wachter, Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains, in: Application of Concurrency to System Design (ACSD) 2009, 2008  

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman and Andrzej Wasowski, An Environment for Compositional Design and Analysis of Real Time Systems

Benoit Caillaud, Benoit Delahaye, Kim G. Larsen, Mikkel Larsen Pedersen and Andrzej Wasowski, Compositional Design Methodology with Constraint Markov Chains           

 

WP3: Implementation

2011

L. Brim, J. Chaloupka, L. Doyen, R. Gentilini and Jean-François Raskin, Faster algorithms for mean-payoff games (2011), in: Formal Methods in System Design, 38(97-118)  

Ernst Moritz Hahn, Gethin Norman, David Parker, Björn Wachter and Lijun Zhang, Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems, in: QEST'11, 2011  

Patricia Bouyer, Nicolas Markey, Jörg Olschewski and Michael Ummels, Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited, Laboratoire Spécification et Vérification, ENS Cachan, France, number LSV-11-02, Research Report, 2011            

Remi Jaubert and Pierre-Alain Reynier, Quantitative Robustness Analysis of Flat Timed Automata, in: Proc. 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 229-244, Springer, 2011

2010

Laurent Doyen and Jean-François Raskin, Antichain Algorithms for Finite Automata, in: Tools and Algorithms for the Construction and Analysis of Systems, pages 2-22, Springer Berlin / Heidelberg, 2010     

Emmanuel Filiot, Nayiong Jin and Jean-François Raskin, Compositional Algorithms for LTL Synthesis, in: Automated Technology for Verification and Analysis ATVA10, pages 112-127, Springer Berlin / Heidelberg, 2010            

Patricia Bouyer, Romain Brenguier and Nicolas Markey, Computing Equilibria in Two-Player Timed Games Turn-Based Finite Games, in: Proceedings of the 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), pages 62-76, Springer, 2010       

Paul Gastin and Nathalie Sznajder, Decidability of well-connectedness for distributed synthesis, Laboratoire Spécification et Vérification, ENS Cachan, France, number LSV-10-02, Research Report, 2010

Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin and Szymon Torunczyk, Energy and Mean-Payoff Games with Imperfect Information, in: Computer Science Logic, pages 260-274, Springer Berlin / Heidelberg, 2010        

Laurent Doyen and Jean-François Raskin, Game Theory for the Computer Scientist, chapter Games with, Cambridge University Press, 2010    

Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger and Jean-François Raskin, Generalized Mean-payoff and Energy Games, in: FSTTCS, pages 505-516, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010      

Emmanuel Filiot, Tristan Le Gall and Jean-François Raskin, Iterated Regret Minimization in Game Graphs, in: Mathematical Foundations of Computer Science 2010, pages 342-354, Springer Berlin / Heidelberg, 2010         

Ocan Sankur, Model-checking robuste des automates temporisés via les machines à canaux, Master Parisien de Recherche en Informatique, Paris, France, 2010     

Patricia Bouyer, Romain Brenguier and Nicolas Markey, Nash Equilibria for Reachability Objectives in Multi-player Timed Games, in: Proceedings of the 21st International Conference on Concurrency Theory (CONCUR'10), pages 192-206, Springer, 2010

Patricia Bouyer, Thomas Brihaye and Fabrice Chevalier, O-Minimal Hybrid Reachability Games (2010), in: Logical Methods in Computer Science, 6:1:1            

Benedikt Bollig and Loïc Hélouët, Realizability of Dynamic MSC Languages, in: Proceedings of the 5th International Computer Science Symposium in Russia (CSR'10), pages 48-59, Springer, 2010            

Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen, Martin De Wulf and Thomas A. Henzinger, Strategy Construction for Parity Games with Imperfect Information (2010), in: Information and Computation, 208:10(1206-1220)  

Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink and Holger Hermanns, Synthesis and Stochastic Assessment of Cost-Optimal Schedules (2010), in: Software Tools for Technology Transfer, 12:5(305-318)

2009

Emmanuel Filiot, Jean-François Raskin and Nayiong Jin, An Antichain Algorithm for LTL Realizability (2009), in: CAV'09 - LNCS, 5643(263-277)        

Peter Bulychev, Thomas Chatain, Alexandre David and Kim G. Larsen, Checking simulation relation between timed game automata, in: Proceedings of the 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), pages 73-87, Springer, 2009

Laurent Doyen, Gilles Geeraerts, Jean-François Raskin and Julien Reichert, Realizability of Real-time Logics (2009), in: FORMATS'09 - LNCS, 5813(133-148)

Peter Bulychev, Thomas Chatain, Alexandre David and Kim G. Larsen, Checking simulation relation between timed game automata, in: Proceedings of the 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), pages 73-87, Springer, 2009      

Franck Cassez and Nicolas Markey, Control of Timed Systems, in: Communicating Embedded Systems~-- Software and Design, pages 83-120, Wiley-ISTE, 2009       

Patricia Bouyer, Marie Duflot, Nicolas Markey and Gabriel Renault, Measuring Permissivity in Finite Games, in: Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09), pages 196-210, Springer, 2009   

Alexandre David, Jacob I. Rasmussen, Kim G. Larsen and Arne Skou, Model-based Framework for Schedulability Analysis Using UPPAAL 4.1, Taylor ad Francis, 2009         

A. David, Jacob Illum, Kim G. Larsen and A. Skou, Model-based Framework for Schedulability Analysis using UPPAAL 4.1., chapter 1, CRC Press, 2009  

Franck Cassez, J. J. Jessen, Kim G. Larsen, Jean-François Raskin and Pierre-Alain Reynier, Robust and Optimal Contorllers - An Industrial Case Study, in: To appear in Proceedings of HSCC'09, 2009   

Alexandre David, Kim G. Larsen and Didier Lime, UPPAAL-TIGA 2009: Towards Realizable Strategies, 2009   

A. Dalsgaard, M. C. Olesen, M. Toft, R. R. Hansen and K. G. Larsen, WCET Analysis of ARM Processors using Real-Time Model Checking, in: Doctoral Symposium on Systems Software Verification (DS SSV'09), Real Software, Real Problems, Real Solutions (technical report), 2009   

2008

Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Größer, Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata, in: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), pages 217-226, IEEE Computer Society Press, 2008       

Patricia Bouyer, Thomas Brihaye, Marcin Jurdzi'nski, Ranko Lazi'c and Michaþ Rutkowski, Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets, in: Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08), pages 63-77, Springer, 2008            

S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund and K. Narayan Kumar, Distributed Timed Automata with Independently Evolving Clocks, in: Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08), pages 82-97, Springer, 2008           

Thomas Bøgholm, Henrik Kragh-Hansen, Petur Olsen, Bent Thomsen and Kim Guldstrand Larsen, Model-based schedulability analysis of safety critical hard real-time Java programs, in: JTRES, pages 106-114, 2008

Patricia Bouyer, Ed Brinksma and Kim G. Larsen, Optimal Infinite Scheduling for Multi-Priced Timed Automata (2008), in: Formal Methods in System Design, 32:1(2-23)   

Alexandre David, Piotr Kordy, Kim G. Larsen and Jan Willen Polderman, Practical Robustness Analysis of Timed Automata, 2008         

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Nicolas Markey, Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, in: QEST'08, Saint-Malo, France, pages 55-64, IEEE Computer Society Press, 2008           

Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier, Robust Analysis of Timed Automata via Channel Machines, in: Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 157-171, Springer, 200      

Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin, Robust Safety of Timed Automata (2008), in: Formal Methods in Computer Design, 33:1-3(45-84)        

Mani Swaminathan, Martin Fraenzle and Joost-Pieter Katoen, The Surprising Robustness of (Closed) Timed Automata against Clock-Drift, in: 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2008   

2007

M. Schoeberl, H. Sondergaard, B. Thomsen and A. P. Ravn., A profile for safety critical java, in: ISORC07: Proceedings of the 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, pages 94-101, 2007       

 

WP4: Testing

2011

Carsten Rütz and Julien Schmaltz, An Experience Report on an Industrial Case-Study about Timed Model-Based Testing with UPPAAL-TRON, in: A-MOST'07: 7th Int. Workshop on Advances in Model-Based Testing, IEEE CS, 2011   

Fides Aarts, F. Heidarian, P. Olsen and Frits Vaandrager, Automata Learning Through Counterexample-Guided Abstraction Refinement, 2011           

Yingke Chen, Hua Mao, Manfred Jaeger, Thomas D. Nielsen, Kim G. Larsen and Brian Nielsen, Learning Probabilistic Automata for Model Checking, in: The Eighth International Conference on Quantitative Evaluation of SysTems (QEST 2011). Accepted., 2011    

Mark Timmer, Ed Brinksma and Marielle Stoelinga, Model-Based Testing, chapter 1, pages 1-32, IOS Press, NATO Science for Peace and Security Series D: Information and Co, volume 30, 2011  

Jan Tretmans, Model-Based Testing and Some Steps towards Test-Based Modelling, in: SFM 2011, pages 297-326, Springer-Verlag, 2011    

Alexandre David, Kim G. Larsen, Shuhao Li, Marius Mikucionis and Brian Nielsen, Testing Real-Time Systems under Uncertainty (2011), in: LNCS (Submitted to Post-conference proceedings for FMCO'2010)           

Ralf Mitsching, Frank Fiedler, Henrik Bohnenkamp, Carsten Weise and Stefan Kowalewski, TripleT: Improving Test Responsiveness for High Performance Embedded Systems, in: Proc. 4th IEEE International Conference on Software Testing, Verification, and Validation, 2011

2010

Sabrina von Styp, Henrik Bohnenkamp and Julien Schmaltz, A Conformance Testing Relation for Symbolic Timed Automata, in: Proc. FORMATS 2010, pages 243-255, Springer-Verlag, 2010        

Jan Tretmans, A Theory of Model-Based Testing, and How ioco Goes eco, pages 86-89, Elsevier, 2010            

Shuhao Li, Games and Scenarios for Real-Time System Validation, Dept. of Computer Science, Aalborg University, 2010         

Fides Aarts, B. Jonsson and J. Uijen, Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction, in: 22nd IFIP International Conference on Testing Software and Systems, Natal, Brazil, November 8-10, Proceedings, pages 188-204, Springer, 2010        

Fides Aarts, J. Schmaltz and Frits Vaandrager, Inference and Abstraction of the Biometric Passport, in: Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I, pages 673-686, Springer, 2010           

Fides Aarts and Frits Vaandrager, Learning I/O Automata, in: 21st International Conference on Concurrency Theory (CONCUR), Paris, France, August 31st - September 3rd, 2010, Proceedings, pages 71-85, Springer, 2010        

Marius Mikucionis, Online Testing of Real-Time Systems, Dept. of Computer Science, Aalborg University, 2010            

F. Zhu, Testing Timed Systems in Simulated Time with Uppaal-Tron: An Industrial Case Study, Institute for Computing and Information Sciences, Radboud University, 2010

2009

Marielle Stoelinga and Mark Timmer, Interpreting a Successful Testing Process: Risk and Actual Coverage, in: Proceedings of the Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Los Alamitos, pages 251-258, IEEE Computer Society, 2009

Marielle Stoelinga and Mark Timmer, Interpreting a Successful Testing Process: Risk and Actual Coverage, University of Twente, number TR-CTIT-09-17, Technical Report, 2009

W. Mostowski, E. Poll, Julien Schmaltz, Jan Tretmans and R. Wichers Schreur, Model-Based Testing of Electronic Passports, in: Formal Methods for Industrial Critical Systems - FMICS 2009, pages 207-209, Springer-Verlag, 2009              

Alexandre David, Kim Guldstrand Larsen, Shuhao Li and Brian Nielsen, Timed Testing under Partial Observability, in: Proc. 2nd International Conference on Software Testing, Verification and Validation (ICST'09), pages 61-70, IEEE Computer Society, 2009          

2008

Alexandre David, Shuhao Li, Brian Nielsen and Kim G. Larsen, A Game-Theoretic Approach to Real-Time System Testing, in: DATE, pages 486-491, 2008       

Shuhao Li, Alexandre David, Kim G. Larsen and Brian Nielsen, Cooperative Testing of Uncontrollable Timed Systems, in: Fourth Workshop on Model-Based Testing (MBT'08), 2008

Jan Tretmans, Model based testing with labelled transition systems, in: Formal Methods and Testing, pages 1-38, Springer-Verlag, 2008              

Jan Tretmans and Julien Schmaltz, On conformance testing for timed systems, in: 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08), St Malo, France, pages 248-263, Springer, 2008            

Henrik Bohnenkamp and Marielle Stoelinga, Quantitative Testing, in: Proc. EMSOFT 2008, ACM, 2008

Anders Hessel, Marius Mikucionis, Brian Nielsen, Paul Pettersson, Arne Skou and Kim G. Larsen, Testing Real-Time Systems Using UPPAAL, LNCS, volume 4949, 2008

 

WP5: Case Studies, Tools, Dissemination and Exploitation

2011

Hernán Baró Graf, Holger Hermanns, Juhi Kulshrestha, Jens Peter, Anjo Vahldiek and Aravind Vasudevan, A Verified Dependable Wireless Safety Critical Hard Real-Time Design, in: 12th IEEE International Symposium on a World of Wireless, Mobile and Multimedia Networks (WoWMoM) (IEEE WoWMoM 2011), 2011

Carsten Rütz and Julien Schmaltz, An Experience Report on an Industrial Case-Study about Timed Model-Based Testing with UPPAAL-TRON, in: A-MOST'07: 7th Int. Workshop on Advances in Model-Based Testing, IEEE CS, 2011   

Haidi Yue, Henrik Bohnenkamp, Malte Kampschulte and Joost-Pieter Katoen, Analysing and Improving Energy Efficiency of Distributed Slotted Aloha (2011), in: NEW2AN 2011  

Benoit Delahaye, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen and Andrzej Wasowski, APAC: a tool for reasoning about Abstract Probabilistic Automata, 2011        

Marten Sijtema, Marielle Stoelinga, Axel Belinfante and Lawrence Marinelli, Experiences with Formal Engineering: Model-based Specication, Implementation and Testing of a Software Bus at Neopost., in: Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems, Springer, 2011           

J. Berendsen, B. Gebremichael, Frits Vaandrager and M. Zhang, Formal Specification and Analysis of Zeroconf using Uppaal (2011), in: ACM Transactions on Embedded Computing Systems, 10:3       

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski, Timothy Bourke and Didier Lime, New Results on Timed Specifications, 2011

Andreas E. Dalsgaard, Rene R. Hansen, Kenneth Y. Jørgensen, Kim G. Larsen, Mads C. Olesen, Petur Olsen and Jiri Srba, OPAAL: A Lattice Model Checker, 2011   

Mark Timmer, SCOOP: A Tool for SymboliC Optimisations Of Probabilistic Processes, in: Proceedings of the 8th International Conference on Quantitative Evaluation of SysTems, IEEE Computer Society, 2011            

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny B. Poulsen, Jonas V. Vliet and Zheng Wang, Statistical Model Checking for Networks of Priced Timed Automata, 2011

Joost-Pieter Katoen, Ivan S. Zapreev, E. Moritz Hahn, Holger Hermanns and David N. Jansen, The Ins and Outs of the Probabilistic Model Checker MRMC (2011), in: Performance Evaluation, 68:2(90-104)          

2010

J. Berendsen, Abstraction, Prices and Probability in Model Checking Timed Automata, Radboud University Nijmegen, 2010          

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman and Andrzej Wasowski, An Environment for Compositional Design and Analysis of Real Time Systems, 2010   

Haidi Yue, Henrik Bohnenkamp and Joost-Pieter Katoen, Analyzing Energy Consumption in a Gossiping MAC Protocol, in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB/DFT), pages 107-119, Springer-Verlag, 2010       

Marijn R. Jongerden, Alexandru Mereacre, Henrik Bohnenkamp, Boudewijn R. Haverkort and Joost-Pieter Katoen, Computing Optimal Schedules for Battery Usage in Embedded Systems (2010), in: IEEE Transactions on Industrial Informatics, 6:3(276-286)      

Jiansheng Xing, Bart Theelen, Rom Langerak, Jaco van de Pol, Jan Tretmans and Jeroen Voeten, From POOSL to UPPAAL: Transformation and Quantitative Analysis, in: ACSD 2010: Int. Conf. on Application of Concurrency to System Design, pages 47-56, IEEE Computer Society Press, 2010           

Haidi Yue and Joost-Pieter Katoen, Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption, in: 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA), pages 247-261, 2010        

Jacob Illum, Kim G. Larsen, Marius Mikucionis and Steen Palm, Model-Based Approach for Schedulability Analysis, 2010            

T. Basten, Benthum E. van, M. Geilen, M. Hendriks, F. Houben, G. Igna, F. Reckers, Smet S. de, L. Somers, E. Teeselink, N. Trcka, Frits Vaandrager, J. Verriet, M. Voorhoeve and Y. Yang, Model-Driven Design-Space Exploration for Embedded Systems: The Octopus Toolset, in: Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I, pages 90-105, Springer, 2010  

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, PASS: Abstraction Refinement for Infinite Probabilistic Models, in: TACAS, 2010          

Holger Hermanns, Kim G. Larsen, Jean-François Raskin and Jan Tretmans, Quantitative System Validation in Model Driven Design, in: EMSOFT: Embedded Systems Week, Compilation Proceedings, pages 301-302, ACM, 2010   

Marius Mikucionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Steen Ulrik Palm, Jan Storbank Pedersen and Poul Hougaard, Schedulability Analysis Using Uppaal: Herschel-Planck Case Study, in: Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece,, pages 175-190, Springer, 2010            

F. Zhu, Testing Timed Systems in Simulated Time with Uppaal-Tron: An Industrial Case Study, Institute for Computing and Information Sciences, Radboud University, 2010   

Jiansheng Xing, Bart Theelen, Rom Langerak, Jaco van de Pol, Jan Tretmans and Jeroen Voeten, UPPAAL in Practice: Quantitative Verification of a RapidIO Network, in: ISoLA 2010 - Part II: Leveraging Applications of Formal Methods, Verification, and Validation, pages 160-174, Springer-Verlag, 2010         

Arild Haugstad, Alexandre David and Kim G. Larsen, UPPAAL PRO: A Tool for Performance Analysis of Probabilistic Timed Automata, 2010  

G. Igna and Frits Vaandrager, Verification of Printer Datapaths Using Timed Automata, in: Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II, pages 412-423, Springer, 2010

2009

Arnd Hartmanns and Holger Hermanns, A Modest Approach to Checking Probabilistic Timed Automata, in: Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 187-196, IEEE Computer Society, 2009

I. AlAttili, F. Houben, G. Igna, S. Michels, F. Zhu and F. W. Vaandrager, Adaptive Scheduling of Data Paths using Uppaal Tiga, in: Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications (QFM'09), pages 1-12, 2009       

F. Heidarian, J. Schmaltz and F. W. Vaandrager, Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks, in: Proceedings 16th International Symposium of Formal Methods (FM2009), Eindhoven, the Netherlands, November 2-6, 2009, pages 516-531, Springer, 2009

Muhammad Saleem Vighio and Anders Peter Ravn, Analysis of collisions in wireless sensor networks, in: Proceedings of 21st Nordic Workshop on Programming Theory, 2009       

Stephan Roolvink, Anne Remke and Marielle Stoelinga, Dependability and Survivability Evaluation of a Water Distribution Process with Arcade, in: Proceedings of the 9th International Workshop on Performability of Computer and Communication Systems, pages 4-7, 2009       

Hichem Boudali, Andre Nijmeijer and Marielle Stoelinga, DFTSim: A Simulation Tool for Extended Dynamic Fault Trees, in: Proceedings of the 42nd Annual Simulation Symposium, 2009

Jonathan Bogdoll, Holger Hermanns and Lijun Zhang, FlowSim Simulation Benchmarking Platform, in: Sixth International Conference on the Quantitative Evaluation of Systems, pages 211-212, IEEE Computer Society, 2009            

Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, Springer, 2009       

J. Berendsen, D. N. Jansen and F. W. Vaandrager, Fortuna: Model Checking Priced Probabilistic Timed Automata, Institute for Computing and Information Sciences, Radboud University Nijmegen, Report, 2009  

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter and Lijun Zhang, INFAMY: An Infinite-State Markov Model Checker, in: CAV, pages 641-647, Springer Verlag, 2009   

Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp and Joost-Pieter Katoen, Maximizing System Lifetime by Battery Scheduling, in: 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, IEEE Computer Society, 2009     

Ulrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Michael A. Petersen and Arne Skou, Model-Based GUI Testing Using Uppaal at Novo Nordisk, in: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, pages 814-818, Springer, 2009       

M. Schuts, F. Zhu, F. Heidarian and F. W. Vaandrager, Modelling Clock Synchronization in the Chess gMAC WSN Protocol, in: Proceedings Workshop on Quantitative Formal Methods: Theory and Applications (QFM'09), pages 41-54, 2009         

Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang, Probabilistic Reachability for Parametric Markov Models, in: SPIN, Grenoble, France, pages 88-106, Springer, 2009      

Franck Cassez, J. J. Jessen, Kim G. Larsen, Jean-François Raskin and Pierre-Alain Reynier, Robust and Optimal Contorllers - An Industrial Case Study, in: To appear in Proceedings of HSCC'09, 2009   

Sandie Balaguer, Specification of Properties using Live Sequence Charts: Theory and Implementation, Department of Computer Science, Aalborg University, Denmark, 2009

Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns and David N. Jansen, The Ins and Outs of The Probabilistic Model Checker MRMC, in: Quantitative Evaluation of Systems (QEST), Budapest, Hungary, pages 167-176, IEEE Computer Society, 2009        

Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll and Marco Roveri, Verification and Performance Evaluation of AADL Models (Tool Demonstration), in: Proc. 7th Joint Meeting of European Software Engineering Conference and ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC/FSE 2009), pages 285-286, ACM Press, 2009

2008

Lijun Zhang, A Space-Efficient Probabilistic Simulation Algorithm, in: Concurrency Theory (CONCUR), pages 248-263, Springer, 2008   

Jonathan Bogdoll, Holger Hermanns and Lijun Zhang, An Experimental Evaluation of Probabilistic Simulation, in: 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), pages 37-52, Springer, 20

David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Marielle Stoelinga and Ivan S. Zapreev, How fast and fat is your probabilistic model checker? An experimental comparison, in: Proceedings of the 3rd Haifa Verification Conference (HVC 2007), Haifa, Israel, pages 69-85, Springer, 20  

Viet Yen Nguyen and Theo C. Ruys, Incremental Hashing for SPIN, in: Proceedings 15th International SPIN Workshop on Model Checking of Software, 2008    

Pepijn Crouzen, Holger Hermanns and Lijun Zhang, On the Minimisation of Acyclic Models, in: CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, pages 295-309, Springer, 2008           

Holger Hermanns, Björn Wachter and Lijun Zhang, Probabilistic CEGAR, in: 20th International Conference on Computer Aided Verification (CAV), pages 162-175, Springer, 2008          

Lijun Zhang, Holger Hermanns, Ernst Moritz Hahn and Björn Wachter, Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains, in: Application of Concurrency to System Design (ACSD) 2009, 2008