Combining formal specification methods and informal specification methods for requirement analysis

In this paper, we advocate an approach to model the required software process with the 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. In this paper, we experiment the combination DFDs method and Interval Temporal Logic for requirement analysis. A particular example, the controller for a system of passenger lifts, is chosen for illustration.