On formal support for industrial-scale requirements analysis

Abstract

Drawing on practical experience in the development of dependable applications, this paper presents a number of “goals” for industrially applicable formal techniques in the specification and analysis of requirements for hybrid systems. These goals stem from domain-specific concerns such as the division between environment, plant and controller; and from the development context with its wide variety of analysis and design activities. Motivated by some of these goals, we present a methodology, based on formal methods, for the requirements analysis of hybrid systems that are safetycritical. This methodology comprises a framework whose stages are based on levels of abstraction that follow a general structure for process control systems, a set of techniques appropriate for the issues to be analysed at each stage of the framework, and a hierarchical structure for the product of the analysis. Some aspects of the methodology are exemplified through two case studies. The extent to which this approach meets the goals espoused earlier is discussed.