Formal Verification Technology For Object-Oriented Software

With the development of information and technology, the software scale and complexity has largely increased. How to improve software quality becomes an important issue. How to guarantee software's accuracy and enhance software's reliability is also a key which people are studying now. In the 20th century 60's, "software crisis" indicated that all questions produced in the software project are up to about 40% or 60% in the requirement stage. In this process, questions include the method fault of collection, compilation, consultation, and the revisional product requirement, and also include the informal information collection, undetermined or ambiguous function, without discoverable or commutative supposition, imperfect requirement documents, or requirement change which may arise suddenly and so on. In order to develop reliable software system, the effective specification method, validation and verification method are necessary.The goal of formal methods is to develop reliable software product. Formal methods can help to discover inconsistency or ambiguity in system description that other means are not easy to find. Formal method includes formal specification and formal verification. Theorem proving is a formal verification via extracting properties that the specification should hold, expressing theorem form and proving them using some proof tools.Formal specification language Object-Z is an Object-Oriented extension for the formal specification language Z, based on mathematical logic and set theory, which can describe large-scale Object-Oriented software precisely and may carry on formal inference to guarantee accuracy and consistency. Object-Z can describe general Object-Oriented formal specification, but can't describe the specification with some special property properly, such as behavioral subtyping inheritance. Object-Z does not maintain behavioral subtyping usually. This paper presents a method to describe Object-Oriented formal specification with behavioral subtyping inheritance. Behavioral subtyping inheritance is one kind of strong subtyping inheritance which has good properties that the verified specification suits to the substituted specification and it does not need verify again. In order to strengthen complex system inference ability, we may use the known information directly. Thus, we can reuse the specification and the verification. Safety-critical system has function requirement and time requirement frequently. Precise requirement for real-time system is essential, but Object-Z is difficult to describe Object-Oriented real-time software system. In this paper, we propose two real-time extension methods for Object-Z: separation method which separates function part from real-time part, extending Object-Z method with linear temporal logic with clocks. After extending, Object-Z can describe or verify Object-Oriented real-time software system conveniently.Polymorphism is an important concept for Object-Oriented programming. It can use a subclass object to replace its supclass object. When applying an operation of the supclass object, it will call the homonymy operation defined in the subclass automatically. This paper gives polymorphic inference for Object-Oriented specification. We can reason about polymorphism with the inference rules and reuse the inference.If a formal specification is usable, it should be consistent or inconflictive. This paper gives a verification method to check the properties that a formal specification should hold. Especially, it discusses how to generate relevant proof obligations(PO) to be proven, which aims to check consistency for the formal specification, that is, whether formal specification holds the relevant properties. If a proof obligation can be proven, then the part referred to in the specification is consistent.Designing and developing verification tool have vital significance to enhance verification efficiency, improve software development process, and guarantee software quality. In this paper, we design a generator of proof obligation for Object-Z specification, which can generate relevant proof obligations. Firstly, it can input the file from Object-Z editor into the generator. Then, the generator can generate proof obligation that prover Z/EVES can identify the format. All the files hold Latex format.