The Observer-based Technique for Requirements Validation in Embedded Real-time Systems

Model-based requirements validation is an increasingly attractive approach to discovering hidden flaws in requirements in the early phases of systems development life cycle. The application of using traditional methods such as model checking for the validation purpose is limited by the growing complexity of embedded real-time systems (ERTS). The observer-based technique is a lightweight validation technique, which has shown its potential as a means of validating the correctness of model behaviors. In this paper, the novelty of our contributions is three-fold: 1) we formally define the observer constructs for our formal specification language namely the Timed Abstract State Machine (TASM) language and, 2) we propose the Events Monitoring Logic (EvML) to facilitate the observer specification and, 3) we show how to execute observers to validate the requirements describing the functional behaviors and non-functional properties (such as timing) of ERTS. We also illustrate the applicability of the extended TASM language through an industrial application of a Vehicle Locking-Unlocking system