Postdoc position
Runtime validation of timed systems
| Keywords | : |
timed systems, runtime validation, enforcement, model based testing, test purpose, test generation, timed traces
|
Terms
Title: Runtime validation of timed systems
Duration: 12 months
Type: Postdoc position
Salary (take-home pay): 2100 Euros / month
Contact
Antoine Rollet
LaBRI - University of Bordeaux
(+33)5 40 00 35 34
email: rollet__AT__labri.fr
Context
Timed systems are often used in critical systems and need to be carefully validated. Validation of systems is a very wide domain of research with many results, but the fact of adding time aspects usually leads to new difficulties and specific technics.
Runtime validation mainly includes different domains: verification of properties at runtime, enforcing properties at runtime, and properties testing.
- Runtime verification: a "monitor" is used to check if an execution trace (obtained one by one or entirely) verifies a property P without modifying the general execution of the system. Compared to many testing approaches, we do not need the specification of the system, only the property to verify. Now "Runtime verification" is a specific research domain ([Hav00], [HR01], [HR02], [LKK+99], [LS08]).
- Runtime enforcement: may be seen as an extension of the previous approach. The monitor (called now enforcer) can be seen as a kind of "filter". It is now equipped with a memory and is able to store the events. If it is possible, it releases the actions assuring that the required property P is verified. In this case, the enforcer modifies the general execution of the system. Output sequences of the enforcer have to be "correct" (sequence verifies property P) and "transparent" (correct input sequences are not modified). More details can be found in [HMS06], [Sch00], [Vis00], [LBW09], [LBW05], [Fal09].
- Properties testing: since using only the specification to generate tests may often lead to infinite test cases, it is possible to use a property (added to the specification) to drive the test generation. Many test purpose approach have been proposed (e.g. [JJ05]) and some for timed systems ([BJSK11]) modelled with timed automata [AD94].
Subject:
In a general way, the objective of this postdoc position is to extend runtime validation technics in the context of timed systems.
Considering "timed enforcement", a difficulty is that the instant of occurrence of an event has to be considered by the enforcer. The storing time has to be saved, and the monitor has to decide the instant of dumping an event according to the timed property P. Some questions could be investigated: considering now timed traces, and the timed property P (described as a timed automaton for example), how to generate a timed enforcer? Which model? How to define the new notion of transparency?
In this position, the domain of Test Generation based on Test Purpose for timed systems may also be investigated.
Theoretical results may be implemented in a tool in order to prove the relevance of the approaches.
This project is financed by the French National Research Agency (ANR, VACSIM Project) and includes several academic and industrial partners (INRIA Rennes, I3S, Lurpa, EDF R&D, Dassault Systemes). It follows the TESTEC ANR Project about validation of critical systems with the same partners.
Prerequies:
The candidate should have a strong knowledge of formal models (automata) and formal methods such as verification and/or model based testing (PhD level). A competence in timed models such as timed automata and/or in runtime enforcement would be a real advantage.
References:
[AD94] Rajeev Alur and David L. Dill.
"A Theory of Timed Automata".
Theoretical Computer Science 126(2), pages 183-235, 1994.
[Hav00] Klaus Havelund.
"Using runtime analysis to guide model checking of Java programs".
In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pages 245-264, London, UK, 2000. Springer-Verlag.
[HR01] Klaus Havelund and Grigore Rosu.
"Monitoring java programs with Java PathExplorer".
Technical report, RIACS, 2001.
[HR02] Klaus Havelund and Grigore Rosu.
"Synthesizing monitors for safety properties".
In TACAS '02 : Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 342-356, London, UK, 2002. Springer-Verlag.
[LKK+99] Insup Lee, Sampath Kannan, Monjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan.
"Runtime assurance based on formal specifications".
In In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999.
[LS08] Martin Leucker and Christian Schallhart.
"A brief account of runtime verification".
Journal of Logic and Algebraic Programming, 78(5) :293-303, may/june 2008.
[HMS06] Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider.
"Computability classes for enforcement mechanisms".
ACM Trans. Program. Lang. Syst., 28(1) :175-205, 2006.
[Sch00] Fred B. Schneider.
"Enforceable security policies".
ACM Trans. Inf. Syst. Secur., 3 1) :30-50, 2000.
[Vis00] Mahesh Viswanathan.
"Foundations for the run-time analysis of software systems".
PhD thesis, University of Pennsylvania, Philadelphia, PA, USA, 2000.
[LBW09] Jay Ligatti, Lujo Bauer, and David Walker.
"Run-time enforcement of nonsafety policies".
ACM Transactions on Information and System Security, 12(3) :1-41, January 2009.
[LBW05] Jay Ligatti, Lujo Bauer, and David Walker.
"Enforcing Non-safety Security Policies with Program Monitors".
In ESORICS, pages 355-373, 2005.
[Fal09] Ylies Falcone
"Etude et mise en oeuvre de techniques de validation à l'exécution"
Phd thesis, University of Grenoble 1, France
[JJ05] Claude Jard and Thierry Jeron.
"Tgv : theory, principles and algorithms".
International Journal on Software Tools for Technology Transfer (STTT), 7(4) :297-315, 2005.
[BJSK11] N. Bertrand, T. Jéron, A. Stainer and M. Krichen.
"Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata".
In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), Saarbrücken, Germany, April 2011. LNCS 6605, pages 96-111. Springer.
[NR11] O. Nguena-Timo and A. Rollet
Test Selection for Data-Flow Reactive Systems based on Observations
In 7th Workshop on Advances in Model Based Testing A-MOST 2011, March 21, 2011, Berlin, Germany, 8p.
[NMR10] O. Nguena Timo and H. Marchand and A. Rollet
Automatic Test Generation for Data-Flow Reactive Systems with time constraints
In 22nd IFIP International Conference on Testing Software and Systems (ICTSS10), (ex Testcom/Fates), November 8-12, 2010, Natal, Brazil, 6p. (short paper)