Combining formal specification methods and informal specification methods for requirement analysis

摘要

We advocate an approach to model a required software process with structured methods, and then to apply formal analysis procedures to the model in order to ensure that the software requirements model satisfies required system function and performance goals and constraints, including safety. We experiment with the combination DFD method and interval temporal logic for requirements analysis. A particular example, the controller for a system of passenger lifts, is chosen for illustration.