A logical model checker can be an e ffective tool for veri cation of software applications.
However, these kind of tools are rarely used, as the requirements specifi cation use a cumbersome textual notation, such as LTL.
Previous work on the development of the TimeLine formalism shows how these tools can be made more accessible in many context.
This paper describes how this formalism can be used to visually defi ne safety specifi cations, and which is the meaning by mapping it to state automaton.
Keywords: TimeLine formalism, model-checking, state automaton, run-time monitoring
A logical model checker can be an effective tool for verification of software applications.
However, these kind of tools are rarely used, as the requirements specification use a cumbersome textual notation, such as LTL.
Previous work on the development of the TimeLine formalism shows how these tools can be made more accessible in many context. This work shows how the Timeline formalism can be used to visually define safety specifications in AToMPM, then transformed into finite automaton for static checks on the output trace of an example Chatroom application.
The final product allows for easily definable safety specification, which can produce powerful temporal checker using model-transformations and code-generation.
Keywords: TimeLine formalism, model-checking, state automaton, trace validation, model-transformation, AToMPM