《Tools for Formal Specification, Verification, and Validation of Requirements.docx》由会员分享，可在线阅读，更多相关《Tools for Formal Specification, Verification, and Validation of Requirements.docx（52页珍藏版）》请在金锄头文库上搜索。
1、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 Laborator
2、y,Washington,DC20375heitmeyer,kirby,labawhttp:/ 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 excepti
3、on 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,
4、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 detecte
5、d 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 deca
6、de,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 tounderstan
7、d 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 develop
8、ers?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
9、 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
10、 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
11、?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?catio
12、n 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
13、 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 mus
14、t 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 contro
15、l 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 beh
16、avior 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
