Computer science as a field has not yet produced a general method to mechanically transform complex computer system requirements into a provably equivalent implementation. Such a method would be one major step towards dealing with complexity in computing, yet it remains the elusive "holy grail" of system development. 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 such tools and methods leave unfilled is that the formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the classes of complex systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations. While other techniques are available, this method is unique in offering full mathematical tractability while using notations and techniques that are well known and well trusted. We illustrate the application of the method to an example procedure from the Hubble Robotic Servicing Mission currently under study and preliminary formulation at NASA Goddard Space Flight Center.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal requirements-based programming for complex systems


    Contributors:
    Rash, J.L. (author) / Hinchey, M.G. (author) / Rouff, C.A. (author)


    Publication date :

    2005


    Size :

    10 Seiten, 21 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Formal verification of safety requirements on complex systems

    Bernardeschi, C. / Fantechi, A. / Gnesi, S. | Tema Archive | 1996




    Application of Formal Methods to Scenario-based Requirements Engineering

    Babin, G. / Lustman, F. | British Library Online Contents | 2001


    Formal Requirements Analysis Techniques for Software-Intensive Automotive Electronic Control Systems

    Rao, A.C. / Dixit, M.G. / Sethu, R. et al. | British Library Conference Proceedings | 2011