Requirements to Design to Code:Towards a Fully Formal Approach to Automatic Code Generation Michael G.Hinchey1James L.Rash1Christopher A.Rouff2
November30,2004
1Information Systems Division2SAIC
Code580Suite300
NASA Goddard Space Flight Center4001N.Fairfax Drive
Greenbelt,MD20771Arlington,V A22203 {hinchey,james.l.rash}@v
togethersoftmanager是什么Abstract
A general-purpo method to mechanically transform system require-
ments into a provably equivalent model has yet to appear.Such a method
just a dream歌词reprents a necessary step toward high-dependability system engineering
for numerous possible application domains,including nsor networks and
autonomous systems.Currently available tools and methods that start with
a formal model of a system and mechanically produce a provably equivalent
implementation are valuable but not sufficient.The“gap”that current tools
and methods leave unfilled is that their formal models cannot be proven to
be equivalent to the system requirements as originated by the customer.For
the class of systems who behavior can be described as afinite(but sig-
nificant)t of scenarios,we offer a method for mechanically transforming
requirements(expresd in restricted natural language,or in other appropri-
ate graphical notations)into a provably equivalent formal model that can be
ud as the basis for code generation and other transformations.
Key Words:Validation,verification,formal methods,automatic code generation, nsor networks
Contents
najie1Introduction2
1
2Problem Statement2
2.1Specifications,Models,and Designs (3)
2.2A Novel Approach (5)
3Technical Approach6
3.1R2D2C (6)
3.2Short-cut R2D2C (9)
acai4A Simple Example10grand canyon
4.1Specification of LOGOS (11)
5Application Areas14 6Related Work15 7Conclusions and Future Work16 1Introduction
Sensor networks and other highly distributed autonomous systems cannot attain high dependability without addressing software dependability issues.Develop-ment of a system that will have a high level of reliability requires the developer to reprent the system as a formal model that can be proven to be correct.Through the u of currently available tools,the model can then be automatically trans-formed into code with minimal or no human intervention to reduce the chance of inadvertent inrtion of errors by developers.Automatically producing the formal model from customer requirements would further reduce the chance of inrtion of errors by developers.
The need for ultra-high dependability systems increas continually,along with a correspondingly increasing need to ensure correctness in system development. By“correctness”,we mean that the implemented system is equivalent to the re-quirements,and that this equivalence can be proved mathematically.
Available system development tools and methods that are bad on formal models provide neither automated generation of the models from requirements nor automated proof of correctness of the models.Therefore,today there is no automated means to produce a system or a procedure that is a p
rovably correct implementation of the customer’s requirements.Further,requirements engineering as a discipline has yet to produce an automated,mathematics-bad process for requirements validation.
2
2Problem Statement
Automatic code generation from requirements has been the ultimate objective of software engineering almost since the advent of high-level programming languages, and calls for a“requirements-bad programming”capability have become deafen-ing[Har04].Several tools and products exist in the marketplace for automatic code generation from a given model.However,they typically generate code,portions of which are never executed,or portions of which cannot be justified from either the requirements or the model.Moreover,existing tools do not and cannot overcome the fundamental inadequacy of all currently available automated development ap-proaches,which is that they include no means to establish a provable equivalence between the requirements stated at the outt and either the model or the code they generate.fxf>对我而言
Traditional approaches to automatic code generation,including tho embod-ied in commercial produ
cts such as Matlab[Mat00],in system development toolts such as the B-Toolkit[LH96]or the VDM++toolkit[IFA00],or in academic re-arch projects,presuppo the existence of an explicit(formal)model of reality that can be ud as the basis for subquent code generation(e Figure1(a)). While such an approach is reasonable,the advantages and disadvantages of the various modeling approaches ud in computing are well known and certain mod-els can rve well to highlight certain issues while suppressing other less relevant details[Par95].It is clear that the conver is also true.Certain models of reality, while successfully detailing many of the issues of interest to developers,can fail to capture some important issues,or perhaps even the most important issues.Existing rever-engineering approaches suffer from a similar plight.In typical approaches, such as the one illustrated in Figure1(b),a model is extracted from an existing system and is then reprented in various ways,for example as a digraph[McL92]. The re-engineering process then involves using the resulting reprentation as the basis for code generation,as above.
2.1Specifications,Models,and Designs
The model on which automatic code generation is bad is referred to as a de-sign,or more correctly,a design specification.There is typically a mismatch be-tween the design and the implementation(sometimes termed the“specification-implementation gap”)in that the process of goin
g from a suitable design to an implementation involves many practical decisions that must be made by the auto-mated tool ud for code generation without any clear-cut justifications,other than the predetermined implementation decisions of the tool designers.There is a more problematic“gap”,termed the“analysis-specification gap”,that emphasizes the
3
relatives是什么意思(a) traditional development process
(b) rever engineering process
Figure1:(a)traditional software development process from requirements to code,and(b)rever engineering from code to a system description.
4
problem of capturing requirements and adequately reprenting them in a specifica-tion that is clear,conci,and complete.This specification must be formal,or proof of correctness is impossible[B
au80].Unfortunately,there is reluctance by many to embrace formal specification techniques,believing them to be difficult to u and apply[Hal90][BH95],despite many industrial success stories[HB95][HB99].
Our experience at NASA Goddard Space Flight Center(GSFC)has been that while engineers are happy to write descriptions as natural language scenarios,or even using mi-formal notations such as UML u cas,they are loath to un-dertake formal specification.Abnt a formal specification of the system under consideration,there is no possibility of determining any level of confidence in the correctness of an implementation.More importantly,we must ensure that this for-mal specification fully,completely,and consistently captures the requirements t forth at the outt.Clearly,we cannot expect requirements to be perfect,complete, and consistent from the outt,which is why it is even more important to have a formal specification,which can highlight errors,omissions,and conflicts.The for-mal specification must also reflect changes and updates from system maintenance as well as changes and compromis in requirements,so that it remains an accurate reprentation of the system.
2.2A Novel Approach
Our approach involves providing a mathematically tractable round-trip engineering approach to system development.The approach described herein is provisionally named R2D2C(“Requirements to Design to Code”).
In this approach,engineers(or others)may write specifications as scenarios in constrained(domain-specific)natural language,or in a range of other notations(in-cluding UML u cas).The will be ud to derive a formal model(Figure??) that is guaranteed to be equivalent to the requirements stated at the outt,and which will subquently be ud as a basis for code generation.The formal model can be expresd using a variety of formal methods.Currently we are using CSP, HoareÕs language of Communicating Sequential Process[Hoa78][Hoa85],which is suitable for various types of analysis and investigation,and as the basis for fully formal implementations as well as for u in automated test ca generation,etc.
3Technical Approach蔬菜销售
R2D2C is unique in that it allows for full formal development from the outt,and maintains mathematical soundness through all phas of the development process, from requirements through to automatic code generation.The approach may also
5
Figure2:The R2D2C approach,generating a formal model from requirements and producing code from the formal model,with automatic rever engineer-ing.
be ud for rever engineering,that is,in retrieving models and formal specifica-tions from existing code,as shown in Figure??.The approach can also be ud to “paraphra”(in natural language,etc.)formal descriptions of existing systems.In addition,the approach is not limited to generating high-level code.It may also be ud to generate business process and procedures,and we are currently experi-menting with using it to generate instructions for robotic devices to be ud on the Hubble Robotic Servicing Mission(HRSM).We are also experimenting with us-ing it as a basis for an expert system verification tool,and as a means of capturing expert knowledge for expert systems.Such potential applications will be described in Section5.
Section3.1describes the approach at a relatively high level.Section3.2de-scribes an intermediate version of the approach for which we have built a prototype tool,and with which we have successfully undertaken some examples.
3.1R2D2C
The R2D2C approach involves a number of phas,which are reflected in the system architecture de
scribed in Figure3.The following describes each of the phas.
D1Scenarios Capture:Engineers,end urs,and others write scenarios describ-ing intended system operation.The input scenarios may be reprented in a constrained natural language using a syntax-directed editor,or may be rep-rented in other textual or graphical formss.
D2Traces Generation:Traces and quences of atomic events are derived from the scenarios defined in D1.
6
