SYNTHESIZING A SPECIFICATION-BASED MONITOR FOR SAFETY REQUIREMENTS

Safety-critical systems such as medical and avionic ones are the systems in whichfailure to satisfy the user requirements may put man’s life and resources in jeopardy. Since theadequate reliability of the software of such systems may be unobtainable via formal methods andthe software testing approach single-handedly, verification of run-time behavior of softwareagainst user requirements violation is considered as a complementary approach. However, thesynthesis of such a run-time verifier, hereafter we have called it a monitor, is confronted with thechallenging problem of verifying low-level run-time behavior of target software against high-leveluser requirements violation. To solve this problem, we propose an approach in two phases. In thefirst phase, we obtain user requirements and then specify their violation formally. This formalspecification is a high-level version of user requirements violations and should be mapped to alow-level one. To this end, in the second phase we extract a tabular automaton from the formalspecification of user requirements violations in order to determine a state-based specification ofthe violations. This low-level specification, which constitutes the core of the monitor, determinesthose states which target software should not reach. To show the effectiveness of our approach, weapply it to the synthesis of a monitor for verifying behavior of the Continuous Insulin InfusionPump (CIIP) system.