| | | Abstracts of Talks and Discussions |
Joint work with Perry R. James, Departamento de Ciencia da Computacao IME-Universidade de Sao Paulo, Sao Paulo, Brazil.
A paper with the above title and authors has now appeared in the Proceedings of 3rd ERCIM International Workshop on Formal Methods for Industrial Critical Systems, FMICS, May 1998. CWI, Amsterdam.
There is now a lot of interest in program testing based on formal specifications. This talk has presented a transposition to full LOTOS of the concepts and terminology developed for algebraic specifications by the Orsay group [1], namely : a notion of "exhaustive test set" is derived from the semantics of the formal notation and from the definition of a correct implementation. Then a finite test set is selected via some "selection hypotheses", which are chosen depending on
This talk defined the exhaustive test sets corresponding to the "red" and "conf" implementation relations, the corresponding verdicts, and discussed the minimal hypothesis required on the implementations under test to ensure that the exhaustive test is unbiased (no correct program is rejected) and valid (only correct program are accepted). After some optimisation, the exhaustive test set obtained for the conf relation turns out to coincide with the must tests used by the Brinksma's group in Twente as a basis for the derivation of tests from full LOTOS specifications [2].
[1] Gaudel M.-C., "Testing can be formal too", invited lecture, TAPSOFT'95, Aarhus, May 1995, LNCS 915, Springer-Verlag, pp. 82-96.
[2] Tretmans J., "A formal approach to conformance testing", PhD thesis, Universiteit Twente, December 1992.
The UniForM Workbench is jointly developed by Universitaet Bremen, Universitaet Oldenburg, and Elpro LET, Berlin. It is a generic framework, instantiated with specific tools for methods to handle communicating distributed systems and real-time requirements. Formalisms (such as Z, CSP+time, and, more recently, CASL) are combined in a logically consistent way by mapping into Isabelle/HOL; this way, transformation rules can be proved correct. The transformation and verification system, based on Isabelle, are demonstrated. The Workbench provides an open framework for control, data and user interface integration: tools are combined as communicating agents; users can work concurrently on the same repository. All tools and the Workbench itself are in the public domain.
Partial information: http://www.informatik.uni-bremen.de/~uniform
Motivated by the need for redefining the application area of some DFG-funded research project, Peter Padawitz proposed to improve the communication about ongoing or finished case studies using formal development methods, in particular algebraic ones.
So please send him messages about your or others' case studies that should be mentioned on the page (padawitz@cs.uni-dortmund.de).
Peter has installed a web page for collecting the information about case studies, see http://ls5.cs.uni-dortmund.de/~peter/CaseStudies.html.
Peter Padawitz gave a talk on coalgebraic versus hidden type specifications and pointed out differences and similarities between both approaches. He presented advanced examples of hidden types such as streams, processes and the operational semantics of a command language where he illustrated syntactic criteria for guaranteeing behavioural congruence.
Peter Mosses presented on-going joint work with Hélène Kirchner towards an algebraic framework with a rich higher-order type system, simple foundations, and a tractable logic. Type-checking is decidable, and well-formed specifications are reduced to unsorted Horn-clause logic with equations and set-membership assertions.
Set-theoretic models are considered, where terms of set type are interpreted extensionally, as well as models where the sets are equipped with labels that serve to distinguish sets whose equality is not a consequence of the specification. Specifications have initial labelled-set models; but deleting the labels may destroy initiality, e.g., when the specification involves equations between terms of set type. The satisfaction of membership assertions is however insensitive to the labels, and it is desirable to eliminate the labels as far as possible, while retaining initiality. One possibility might be to consider reducts where all the set values are simply forgotten, leaving only the atomic objects; this corresponds to the view that types (here, sets) are auxiliary entities, used merely for classifying the specified objects of interest (atomic values, operations).
Compared to higher-order set-theoretic frameworks such as Z and B, the potential advantages of the proposed framework include the possibility of operationalization of the consequences of specifications. Moreover, by allowing the usual set-theoretic operations to be partial, one avoids requiring the carrier to be obtained by a complicated infinitary closure.
A draft paper is in preparation, and will be announced when ready.
| | | Abstracts of Talks and Discussions |