Specification and verification of behavioural properties of fault diagnosis

Properties of physical systems impose behavioural and temporal constraints upon control and diagnosis procedures and programs. It is necessary to specify and verify behavioural and temporal properties of physical systems and their computer programs. To define how time constraints of physical systems effect control and diagnosis programs, these properties should be analysed in two consequent phases. First, properties of physical systems should be specified and verified. Secondly, properties of diagnosis programs should be defined and checked taking into account behavioural and temporal constraints of physical systems. The Petri net-based top-down formalism was selected to specify and verify behavioural and temporal properties of physical systems. To simplify modelling behavioural properties modular blocks were recommended to be used to build up models of physical systems. Using this method there is no need of analysis of properties of the final model. Mathematical description of these blocks was developed and their properties were analysed. Two procedures, “building the normal model” and “building the fault model” and an algorithm “fault path” were elaborated in order to build normal and fault models of physical systems and computer programs, and to define fault paths