rohrs@handel.helios.nd.edu (533) (12/18/90)
I am in the early stages of a literature survey on the topic of formal specification of (software) systems. I'm looking for any suggestions, leads or pointers to survey papers or taxonomies published in the area. I'm also interested in any tutorials, texts, papers, etc. on particular specification "languages" including, but not limited to: SDL, Z, PSL/PSA, SADT, RSL, Anna, IORL, Gypsy, OBJ, and Estelle. Any commentary w.r.t any of the above (or any other specification language or specification system) is welcome. Especially interesting topics inlucde: availability/lack of software tools to support users, ease-of-use, applicability (what kinds of systems can be described by the particular language), "public-domainness", good or bad experiences (using a particular language for particular type of development effort), applicability to demonstrating proof-of-correctness of an implementation, and any other relevant info. If you think the information is already common knowledge in this group, then I'd appreciate an e-mail response. Otherwise, if you think it is of general interest, then by all means please post. If there is any interest, I'll post a summary of the results. Thanx much!! --jon P.S. Please note the e-mail addresses below. jon@trc.tellabs.com jon@ndsun.ee.nd.edu
brianh@ogicse.ogi.edu (Brian Hansen) (12/18/90)
In article <1990Dec17.190909.10829@news.nd.edu> rohrs@handel.helios.nd.edu (533) writes: >I am in the early stages of a literature survey on the topic of formal >specification of (software) systems. I'm looking for any suggestions, leads >or pointers to survey papers or taxonomies published in the area. > >I'm also interested in any tutorials, texts, papers, etc. on particular >specification "languages" including, but not limited to: SDL, Z, PSL/PSA, >SADT, RSL, Anna, IORL, Gypsy, OBJ, and Estelle. I had the opportunity to use the Higher Order Software, Inc, AXES specification language and, though the company is by now defunct, it (AXES) should probably be considered in your taxonomy. There are some offshoots I believe to be commercially available from Hamilton Technology, Inc. of Cambridge Mass. I found it too be a very interesting language/system, but somewhat more time-consuming than normally reasonable. Systems were claimed to be "provably correct", but in one of those apposite twists of fate was written up under a headline of "probably correct system..." -Brian Hansen Oregon Graduate Institute
kremer@cs.utwente.nl (Harro Kremer) (12/19/90)
|> I'm also interested in any tutorials, texts, papers, etc. on particular |> specification "languages" including, but not limited to: SDL, Z, PSL/PSA, |> SADT, RSL, Anna, IORL, Gypsy, OBJ, and Estelle. |> I think you are missing the third Formal Specification Technique standardized by ISO: namely LOTOS. Because of the differences between LOTOS and the mentioned languages, LOTOS should be included in your survey. Harro +----------------------------------------------------------+ | Harro Kremer | | Dept. of Computer Science | | University of Twente | | P.O. Box 217 Email: kremer@cs.utwente.nl | | 7500 AE Enschede voice: +31 53 89 2819 | | Netherlands fax : +31 53 33 3815 | +----------------------------------------------------------+ <No flame yet>
dts@cs.edinburgh.ac.uk (Don Sannella) (12/19/90)
In article <1990Dec17.190909.10829@news.nd.edu>, rohrs@handel.helios.nd.edu (533) writes: > I am in the early stages of a literature survey on the topic of formal > specification of (software) systems. I'm looking for any suggestions, leads > or pointers to survey papers or taxonomies published in the area. > > I'm also interested in any tutorials, texts, papers, etc. on particular > specification "languages" including, but not limited to: SDL, Z, PSL/PSA, > SADT, RSL, Anna, IORL, Gypsy, OBJ, and Estelle. I think the specification language / formal program development framework "Extended ML" deserves to be included in this list. This is for specifying and developing programs in the Standard ML functional programming language, although it is applicable to other programming languages as well. Since I haven't seen anything about it in this group before, I'm posting the following rather than mailing it to rohrs@handel.helios.nd.edu. Anybody interested is welcome to contact me for copies of papers or further details. From the introduction of [ST91] ------------------------------- Extended ML is a framework for the formal development of programs in the Standard ML functional programming language from high-level specifications of their required input/output behaviour. Extended ML is a completely formal framework with a very extensively-developed mathematical basis in the theory of algebraic specifications. It strongly supports ``development in the large'', producing modular programs consisting of an interconnected collection of generic and modular units. The Extended ML framework includes a methodology for formal program development which establishes a number of ways of proceeding from a given specification of a programming task towards a program. Each such step (modular decomposition, etc.) gives rise to one or more proof obligations which must be discharged in order to establish the correctness of that step. The Extended ML language is a wide-spectrum language which encompasses both specifications and executable programs in a single unified framework. It is a simple extension of the Standard ML programming language in which axioms are permitted in module interfaces and in place of code in module bodies. This allows all stages in the development of a program to be expressed in the Extended ML language, from the initial high-level specification to the final program itself and including intermediate stages in which specification and program are intermingled. Formally developing a program in Extended ML means writing a high-level specification of a generic Standard ML module and then refining this specification top-down by means of a sequence (actually, a tree) of development steps until an executable Standard ML program is obtained. The development has a tree-like structure since one of the ways to proceed from a specification is to decompose it into a number of smaller specifications which can then be independently refined further. In programming terms, this corresponds to implementing a program module by decomposing it into a number of independent sub-modules. The end-product is an interconnected collection of generic Standard ML modules, each with a complete and accurate specification of its interface with the rest of the system. The explicit interfaces enable correct reuse of the individual modules in other systems, and facilitate maintainability by making it possible to localize the effect on the system of subsequent changes in the requirements specification. Some recent papers ------------------ D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Barcelona. Springer LNCS 352 (1989). D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park. Springer LNCS, to appear (1990). D. Sannella and A. Tarlecki. Extended ML: past, present and future. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen. Springer LNCS, to appear (1991). Caveats ------- The emphasis in work on Extended ML has mainly been on the FOUNDATIONS of practical formal program development. We are very serious about e.g. providing a complete semantics for the entire specification language, proving that if you do formal program development in the Extended ML framework then your programs really will satisfy the specification you started with, etc. Thus, relatively few case studies have been carried out, and no tools are yet available for working with Extended ML specifications (although work is in progress on these). Until recently, we concentrated on simple first-order total functional programs, but we are now trying to handle all of Standard ML (except for references and assignment), including higher-order functions, polymorphism, exceptions, and non-terminating programs. About Standard ML ----------------- Standard ML is a powerful functional (but not purely functional) programming language with advanced modularisation facilities. See the first two references below for an introduction to Standard ML; the third reference is the complete formal semantics of the language. R. Harper. Introduction to Standard ML. Report ECS-LFCS-86-14, Univ. of Edinburgh. Revised edition (1989). C. Reade. Elements of Functional Programming. Addison-Wesley (1989). R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. MIT Press (1990). Don Sannella University of Edinburgh
weigele@bosun1.informatik.uni-hamburg.de (Martin Weigele) (12/20/90)
In article <1990Dec17.190909.10829@news.nd.edu> rohrs@handel.helios.nd.edu (533) writes: >I am in the early stages of a literature survey on the topic of formal >specification of (software) systems. I'm looking for any suggestions, leads >or pointers to survey papers or taxonomies published in the area. A good starting point for exploration might be Springer's LNCS 428. D. Bjoerner, C.A.R. Hoare and H. Langmaack (eds.): VDM'90: VDM and Z - Formal Methods in Software Development. Three invited talks give some overview (by Dahl, Goguen, Kato et. al) of the field as well as C.A.R. Hoare's preface. Also, lots of lots of references. I am afraid an overview of the kind you request (including all the languages/methods mentioned) has not yet been produced. Martin Weigele, FB Informatik, Uni Hamburg, Germany
new@ee.udel.edu (Darren New) (12/21/90)
In article <1990Dec19.144145@cs.utwente.nl> kremer@cs.utwente.nl (Harro Kremer) writes: >I think you are missing the third Formal Specification Technique >standardized by ISO: namely LOTOS. Actually, to pick a nit, I think only LOTOS and Estelle were standardized by ISO. I think SDL has only been standardized by CCITT. Also, don't forget CHILL and ASN.1 I don't know anything about CHILL. ASN.1 is a language for describing data structures. I don't know how "formal" you would consider it. -- Darren -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, Formal Description Techniques (esp. Estelle), Coffee, Amigas ----- =+=+=+ Let GROPE be an N-tuple where ... +=+=+=
ranga@uceng.UC.EDU (Dr. Ranga R. Vemuri) (12/21/90)
P. Mateti has been developing a language called OM (objects and models) for several years now. His group has specifications of several non-trivial systems written in OM. No survey of formal specification languages is complete without including OM. Mateti can be reached at Professor Prabhaker Mateti Computer Science and Engineering Dept. WSU Research Center Kettering (Dayton) OH 45420 USA Email: pmateti@cs.wright.edu - Ranga