Research On Safety Properties Of Metric Transition Systems

The safety and reliability of software and hardware systems affect the development of various areas of society.Formal verification was proposed to guarantee the correctness of system designs.In the verification,transition systems(Kripke structures)are used to model the systems,and linear-time properties,which are basic properties in specifications,are characterized by the sets of infinite sequences or linear temporal logic(LTL).In particular,linear-time properties contain a kind of important properties,called safety properties,which assert that nothing “bad” happens during execution of systems.The verification of safety properties is the theoretical foundation of the verification of linear-time properties.With the increasing complexity of systems,the quantitative verification of safety properties has attracted much attention from the academic and industrial communities.That is,from verifying whether a system satisfies a given safety property,to measuring what extent a system satisfies the safety property.The theoretical framework of metric transition systems has offered a new research line for the development of the quantitative verification of safety properties.This paper focuses on the extension of safety properties,and the quantitative verification of safety properties over metric transition systems.Our main work is as follows:1.We first give the definition of linear-time properties over metric transition systems,call them metric linear-time properties(MLT-properties),and retain some of their characteristics as much as possible.Then we provide the measure to quantitatively analyze the relationship about satisfaction between metric transition systems and MLT-properties by introducing the distance threshold ?.We define an approximate safety property called?-safety property.Moreover,We give an alternative characterization of ?-safety properties by means of their closure.2.For a special ?-safety property,we reduce the verification of that to the verification of the invariance property by using automata theory,where the invariance property is a special safety property.Then we propose an algorithm to verify whether a metric transition system approximately satisfies an ?-safety property.Further,we introduce an example to illustrate the applicability of our results in practice.3.We extend the definition of LTL in the context of metrics,call it metric linear temporal logic(MLTL),and use MLTL to characterize MLT-properties.Then we discuss the relationship between MLTL and ?-safety properties.These results would provide atheoretical basis for the development of the verification about safety properties in the context of metrics.