FORMAL SPECIFICATION AND VERIFICATION OF REACTIVE SYSTEMS
Kendar Pratap, Manjeet Kaur Bedi · 2013
A system is called reactive, if its role is to maintain an ongoing interaction with its environment. A reactive system changes its actions, outputs and status in response to the input it receives from outside. Reactive systems are used in performing several crucial tasks, where the input that is given to them is vast and, most importantly, unpredictable. In this paper, we propose the specification and verification of reactive systems. The approaches to specification and verification of reactive systems which are different from computational systems are discussed. We have presented the Kripke structure or fair transition system and temporal logic that are most well known techniques for specifying system their properties. Verification can be done through model checking or deductive verification technique depending on the type of reactive system.