Model-based testing and monitoring

This research action targets various problems of testing and monitoring: conformance testing, conformance monitoring, fault detection and diagnosis, state-identification, run-time verification, etc.
We focus on methods which use high-level models with clear semantics. In particular, a large part of this work is done around the model of timed automata. We have been the first, to our knowledge, to propose methods which can fully handle non-deterministic and partially-observable timed automata.

Related papers (read the copyright note)

  1. S. Tripakis. A Combined On-line/Off-line Framework for Black-Box Fault Diagnosis. In RV'09. PDF.

  2. M. Krichen and S. Tripakis. Conformance Testing for Real-Time Systems. In Formal Methods in System Design, vol. 34, num. 3, June 2009, pages 238-304. PDF.

  3. F. Cassez and S. Tripakis. Fault Diagnosis with Static or Dynamic Observers. In Fundamenta Informaticae, vol. 88, 2008, pages 497-540. PDF.

  4. Book chapter: S. Tripakis and T. Dang. Modeling, Verification and Testing using Timed and Hybrid Automata. In P. Mosterman and G. Nicolescu, editors, Model-Based Design for Embedded Systems. CRC Press, 2009. PDF.

  5. Book chapter: F. Cassez and S. Tripakis. Monitoring, Fault-Diagnosis and Testing. In C. Jard and O.H. Roux, editors, Communicating Embedded Systems -- Formal Methods. Hermes, France, 2009.

  6. F. Cassez, S. Tripakis and K. Altisen. Synthesis of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete Event Systems. In TASE'07. Postscript.

  7. F. Cassez, S. Tripakis and K. Altisen. Sensor Minimization Problems with Static and Dynamic Observers for Fault Diagnosis. In ACSD'07. PDF.

  8. K. Altisen, F. Cassez and S. Tripakis. Monitoring and Fault Diagnosis with Digital Clocks. In ACSD'06. Postscript.

  9. M. Krichen and S. Tripakis. State identification problems for finite-state transducers. In FATES-RV'06. Available as VERIMAG Technical Report TR-2005-5.

  10. M. Krichen and S. Tripakis. Interesting properties of the conformance relation tioco. In ICTAC'06.

  11. S. Bensalem, D. Peled, H. Qu and S. Tripakis. Generating path conditions for timed systems. In IFM'05. PDF.

  12. K. Altisen and S. Tripakis. Implementation of timed automata: an issue of semantics or modeling?. In FORMATS'05. A previous version of this paper is available as VERIMAG Technical Report TR-2005-12.

  13. M. Krichen and S. Tripakis. State identification problems for timed automata. In 17th IFIP Intl. Conf. on Testing of Communicating Systems (TestCom'05). PDF.

  14. M. Krichen and S. Tripakis. An Expressive and Implementable Formal Framework for Testing Real-Time Systems. In 17th IFIP Intl. Conf. on Testing of Communicating Systems (TestCom'05). PDF. A previous version of this paper (not containing the BRP case study) is available as VERIMAG Technical Report TR-2004-13.

  15. M. Krichen and S. Tripakis. Real-time testing with timed automata testers and coverage criteria. In Joint conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT'04). Available as VERIMAG Technical Report TR-2004-15.

  16. M. Krichen and S. Tripakis. An Expressive and Implementable Formal Framework for Testing Real-Time Systems. VERIMAG Technical Report TR-2004-13.

  17. M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. In SPIN'04 Workshop on Model Checking Software. PDF.

  18. S. Bensalem, M. Bozga, M. Krichen and S. Tripakis. Testing conformance of real-time applications with automatic generation of observers. In Runtime Verification 2004. PDF.

  19. S. Tripakis. Folk theorems on the determinization and minimization of timed automata. Information Processing Letters, Vol. 99, Issue 6, 30 Sep 2006, Pg 222-226, PDF. A previous version of this paper appeared in FORMATS'03.

  20. S. Tripakis. Fault Diagnosis for Timed Automata. In FTRTFT, 2002. Improved version in PDF.

Teaching:


Back to home page of Stavros Tripakis