Tools for Formal Specification, Verification, and Validation of RequirementsTo appear in Proc.,COMP ASS97Tools for Formal Speci?cation,Veri?cation,and Validation of RequirementsConstance Heitmeyer,James Kirby,and Bruce LabawCenter for High Assurance Computer Systems(Code5546)Naval Research Laboratory,Washington,DC20375heitmeyer,kirby,labawhttp:/www.wendangku.net/doc/0db0612abd64783e09122b10.htmlAbstractAlthough formal methods for developing computer sys-tems have been available for more than a decade,few havehad signi?cant impact in practice.A major barrier to theiruse is that software developers?nd formal methods dif?-cult to understand and apply.One exception is a formalmethod called SCR for specifying computer system require-ments which,due to its easy to use tabular notation and itsdemonstrated scalability,has already achieved some suc-cess in industry.Recently,a set of software tools,includinga speci?cation editor,a consistency checker,a simulator,anda veri?er,has been developed to support the SCR method9,11,5.This paper describes recent enhancements to theSCR tools:a new dependency graph browser which displaysthe dependencies among the variables in the speci?cation,an improved consistency checker which produces detailedfeedback about detected errors,and an assertion checkerwhich checks application properties during simulation.Toillustrate the tool enhancements,a simple automobile cruisecontrol system is presented and analyzed.1.IntroductionAlthough formal methods for developing computer sys-tems have been available for more than a decade,few ofthese methods have had signi?cant impact in the develop-ment of practical systems.A major impediment to the useof formal methods in industrial software development is thewidespread view that the methods are impractical.Not onlydo developers regard most formal methods as dif?cult tounderstand and apply.In addition,they have serious doubtsabout the scalability and cost-effectiveness of the methods.A promising approach to overcoming these problems is tohide the logic languages associated with most formal meth-ods and to adopt a notation,such as a graphical or tabularnotation,that developers?nd easier to user.Speci?cationsin the more“user-friendlynotation can be translated au-tomatically to a form more amenable to formal analysis.Moreover,to scale effectively,a formal method must be2.SCR Method:An Overview2.1.SCR Speci?cationsA recent article by Shaw22presents and discusses a number of different speci?cations of an automobile cruise control system.Each of these speci?cations is constructed to satisfy different objectives.For example,Atlee and Gannon use a logic language to specify the different“modesof the cruise control system4.Their logic language speci?cation is then fed to a model checker that analyzes the speci?cation for violations of selected properties.Another speci?cation of the cruise control system by Smith and Gerhart is rep-resented using the graphical notation of STA TEMA TE and is described by the authors as a“design exercise23.We refer to the former speci?cation as an abstract model and the latter as the STATEMATE speci?cation.One difference between the abstract model,the STA TE-MA TE speci?cation,and an SCR speci?cation of the cruise control system lies in the notation.The abstract model is ex-pressed in a logic language,the STA TEMA TE speci?cation in a graphical notation,and the SCR speci?cation in a tab-ular format.Another difference is the target audience.The abstract model is designed to be processed by a computer, whereas both the SCR speci?cation and the STA TEMA TE speci?cation are engineering documents,designed to be read by software developers.The three speci?cations also differ in a third respectnamely,in the speci?c information each contains about the required system behavior.The objective of the SCR speci?cation is to describe the externally visible behavior of the Cruise Control System. To achieve this,the speci?cation must describe the required relation REQ between the monitored variables,which repre-sent quantities in the environment that the system monitors, and the controlled variables,which represent environmen-tal quantities that the system controls.In the cruise control system,the position of the cruise control lever is an exam-ple of a monitored variable;the position of the throttle is an example of a controlled variable.The REQ relation be-tween the monitored and controlled variables is one of the four relations of the Parnas-Madey Four V ariable Model,a formal framework for describing the required behavior of a computer system20.Atlee and Gannons abstract model is used in veri?cation and,as a result,omits many details of the required system behavior.For example,it does not describe the behavior of the throttle.Because the properties analyzed in4are independent of the throttle behavior and because a model used