| | | Abstracts of Talks |
The abstracts are listed in order of presentation.
Note: Authors who wish to improve the layout of their abstract are welcome to send me a new version using LaTeX mark-up to indicate formatting.
G. Rosu, NASA Ames, and Jose Meseguer, Univeristy of IlinoisPartiality is a fact of life, but at present explicitly partial algebraic specifications lack tools and have limited proof metods. We propose a sound and complete way to support execution and formal reasoning of explicitly partial algebraic specifications within the total framework of membership equational logic (MEL) which has a high-performance interpeter (Maude) and proving tools. This is accomplished by a sound and complete mapping PMEL --> MEL of partial membership equational (PMEL) theories into total ones. Furthermore, we characterize and give proof methods for a class of theories for which this mapping has "almost-zero representational distance," in that the partial theory and its total translation are identical, except for minor syntactic sugar conventions. This then supports very direct execution and formal reasoning of partial theories at the total level. In conjunction with tools like Maude and its proving tools, our methods could be used to execute and reason about partial specifications such as those in the equational sublanguage of CASL.
See also http://ase.arc.nasa.gov/grosu/tapase.html.
(with Hubert Baumeister, Alexander Knapp, Martin Wirsing)The Object Constraint Language (OCL) offers a formal notation for constraining model elements in UML diagrams. OCL consists of a navigational expression language which can be used to state class invariants and pre- and post-conditions of the operations.
In this talk we discuss some problems in ensuring the correctness of programming language implementations (like in Java) with respect to non-local OCL class invariants that are used, for instance, for describing bidirectional associations. As a remedy, we propose a component-based system specification method for using OCL constraints, distinguishing between global component invariants and local class invariants.
The talk is based on the paper OCL Component Invariants by H. Baumeister, R. Hennicker, A. Knapp, M. Wirsing.
Hans-Dieter Ehrich and and Ralf PingerSince its invention some twenty years ago, model checking has become a successful technique for verifying finite-state concurrent systems such as sequential circuit designs or communication protocols. One of the main advantages of model checking over traditional approaches is that the verification is done automatically without any user interaction.Abteilung Informationssysteme,
Technische Universität Braunschweig
Postfach 3329, D-38023 Braunschweig, Germany
{HD.Ehrich/A.Grau/R.Pinger}@tu-bs.de
http://www.cs.tu-bs.de/idb/
When model checking a concurrent system, the global temporal condition is conventionally checked against a sequential state-transition model of the system. This model represents concurrency either by global clock synchronization or by interleaving of its sequential components. In any case, the state space grows exponentially with the number of components. This "state space explosion problem" has been tackled in several ways, including symbolic model checking, partial-order reduction, abstraction, and especially a number of compositionality methods. Very large systems have been successfully checked, demonstrating the power of the techniques.
Compositionality methods are mostly based on the assume-guarantee approach by Misra and Chandy (1981) and Pnueli (1985). Around 1990, several variants were proposed, using different temporal logics and either synchronization or interleaving as composition semantics. The drawback is that these methods are not fully automatic: global conditions must be separated by hand.
We propose a compositionality method separating global conditions automatically into local conditions and communication requirements such that satisfaction of local conditions entails the global condition, provided that the communication requirements are fulfilled. Moreover, we use the more general "perspective concurrency" composition semantics, allowing for synchronization or interleaving in any combination.
The method is based on distributed logic D1 and its translation to D0 as described by Ehrich and Caleiro in Acta Informatica 2000. The method has been completed by Pinger (PhD thesis, 2002), providing an algorithm for matching communication requirements, implementing the method, and showing its practicality with an example of realistic size. The improvements over the only fully automatic method known so far (not implementing assume-guarantee methods) are very promising.
More information and material can be found at http://www.cs.tu-bs.de/idb/.
(with Tom Maibaum)The talk reports on a specification language for OO systems, based on an object-based specification language originally developed by Fiadeiro & Maibaum. The language is based on temporal logic, and differs from standard OO languages in its explicit representation of interactions between instances.
The idea of explicitly describing interactions was first proposed by the software architectures community (also by Rumbaugh in the context of OO programming languages). This technique allows us to express properties of the specified systems in a declarative way.
Our work is related to other formalisms based on the same motivations, notably the work of Fiadeiro's group on (reconfigurable) CommUnity. We feel our work is complementary to theirs, in the sense that our language could provide a (temporal) specification counterpart of the more operational design language CommUnity.
Papers available at http://www.dcs.kcl.ac.uk/staff/aguirre/.
Dominique DUVAL
Université Joseph Fourier, Grenoble.
Dominique.Duval@imag.fr
http://www-lmc.imag.fr/CF/MEMBRES/duval.htmlChristian LAIR
Université Denis Diderot, Paris.
lairchrist@aol.com
Some keywords: specification, meta-specification, projective sketches, adjunction.
In this talk we present a framework for meta-specification, ie. for the specification of specifications. This framework is based on the theory of projective sketches, as introduced by Ehresmann in the 1960's.
Our goal is to study some features of programming languages, like implicit state or subsorting (these applications are not presented here). For this purpose, we need a robust framework for meta-specification. In this talk, we show that such a framework can be based upon projective sketches.
Each projective sketch determines a category of (set-valued) realizations (ie. models). Each propagator (ie. homomorphism of projective sketches) determines an underlying functor between the corresponding categories of realizations. A fundamental theorem about projective sketches (due to Ehresmann, and known as "the associated sheaf theorem") states that this underlying functor has a left adjoint, ie. there is an associated freely generating functor.
It is well known (cf. Mac Lane) that the notions of adjunction and of freely generated structures play a fundamental role in mathematics and computer science.
With respect to any given propagator, we define the diagrammatic notions of specification, domain, and model of a specification with values in a domain. We also define the diagrammatic notions of syntactic entailment and semantic consequence, in such a way that the soundness property is satisfied.
The major new result in this talk deals with the decomposition of propagators. One of its consequences is a sound definition of the diagrammatic notions of inference rules and deduction steps, such that any sequence of deduction steps is a syntactic entailment.
Finally, thanks to many challenging questions and remarks during the talk, there was no time left for looking in detail at equational specifications, nor for outlining some links between our point of view and the logical frameworks based on institutions.
Andrea Corradini and Fabio GadducciThe presentation surveys a recent series of papers by the authors, investigating the categorical foundations of various rule-based formalisms. The starting point is the well-known representation of term rewriting systems as cartesian 2-categories, based on the characterization of finite terms as arrows of a Lawvere (cartesian) theory.
Dipartimento di Informatica, Pisa, Italy
We first show that many term-like structures (including (possibly cyclic) term graphs, µ-terms and rational terms) can be characterized as arrows of suitable theories. Such theories have a structure similar to Lawvere ones, but the set of axioms they satisfy is slightly different. For example, we show that the axiom of naturality of the transformation ! (bang, discharger) corresponds intuitively to "garbage collection", while the naturality of the transformation nabla (duplicator) identifies structures having different degree of sharing. Removing such axioms from the specification of the theory, we get "gs-monoidal" theories, whose arrows are one-to-one with finite term graphs. Theories for the other term-like structures are obtained similarly by adding or removing a few axioms from the specification.
Next, for each of the term-like structures we introduced, we consider rewriting formalisms based on them, and we discuss how to represent them using suitable 2-categories. The outline is the same in all cases: one starts with the theory whose arrows represent the structures of concern, next one adds the cells representing the rules of the system, obtaining a computad, and finally one generates the free 2-category associated with the computad. Cells of the free 2-category can be shown to represent faithfully the rewriting sequences of the original rewriting system. The most delicate point in this construction is to choose the correct encoding of rewriting rules as cells.
The presentation is a summary of the paper:
Corradini, A. and Gadducci, F.: Categorical Rewriting of Term-like Structures, in Proc. GETGRATS Closing Workshop (Bauderon, M. and Corradini, A., eds.), vol. 51 of ENTCS, Elsevier, 2002.
It surveys the following papers by the same authors (available electronically from http://www.di.unipi.it/~gadducci/papers/):
A 2-Categorical Presentation of Term Graph Rewriting, in Proceedings CTCS'97, LNCS 1290, Springer, 1997.
An Algebraic Presentation of Term Graphs, via GS-Monoidal Categories. APCS 7(1999)299-331, Kluwer.
Rewriting on cyclic structures, Tech. Report TR-98-05, Dipartimento di Informatica, Pisa, 1998. Extended abstract in Proceedings of FICS'98.
Rewriting on Cyclic Structures: Equivalence between the Operational and the Categorical Description. TIA 33(1999)467-493.
Rational Term Rewriting, in Proceedings FoSSaCS'98 (Nivat, M., ed.), LNCS 1378(1998)156-171.
Don Sannella, Univ. of EdinburghThe problem of testing modular systems against algebraic specifications is discussed. In particular, we focus on systems where the decomposition into parts is specified by a CASL-style architectural specification and the parts (units) are developed separately, perhaps by an independent supplier. One problem in testing from the unit supplier's point of view is how to test units independently of the context of use. This is most acute for generic units where the particular instantiation cannot be predicted. On the other hand, users of units are concerned with the particular context of use - dictated by the architectural specification at hand - where one concern is how to take advantage of the testing that has already been done by the supplier. Ideas for tackling these problems are presented.
joint work with Patricia Machado, Federal University of Paraiba
(Patricia's home page is http://www.dsc.ufpb.br/~patricia/)
There is a draft paper at http://www.dcs.ed.ac.uk/~dts/pub/arch-test.pdf.
Hartmut Ehrig, Fernando Orejas, Benjamin Braatz, Markus Klein, Martti PiirainenThe paper can be found at the following address: http://www.lsi.upc.es/~orejas/papers/comp.ps.
The aim of this paper is to present a generic component framework for system modeling that could support the development of a wide range of systems mentioned above. In this sense, we have defined a framework that can be used, by providing an adequate instantiation, in connection with a large class of semi-formal and formal modeling techniques. Moreover, the framework is also flexible with respect to the connection of components, providing a compositional semantics of components. This means more precisely that the semantics and internal correctness of a system can be inferred from the semantics of its components. In contrast to other component concepts for data type specification techniques, our component framework is based on a generic notion of transformations. Refinements and transformations are used to express intradependencies, between the export interface and the body of a component, and interdependencies, between the import and the export interfaces of different components. In previous papers the first two authors have presented a conceptual and a formal for an integration paradigm for various kinds of data type and process modeling techniques leading to a generic framework for integrated modeling techniques. The generic component framework in this paper can be especially used for this kind of integrated modeling techniques, like high-level Petri nets. This is shown by explicit examples in this paper. Our generic framework is motivated by main requirements for component-based development in software engineering. It generalizes module concepts for different kinds of Petri nets and graph transformation systems proposed in the literature, and seems to be also suitable for visual modeling techniques, including parts of the UML, if these techniques provide a suitable refinement or transformation concept.
==============================================================================
Statistical or random testing methods are based on a probability distribution on the input domain of a piece of software. This distribution is used to draw arbitrary number of test data, allowing intensive test campaigns.
Various kinds of distributions has been studied: uniform distributions, operational distributions derived from the operational profile of the environment of the future system, or distributions which are derived from the structure of the program or of the specification.
This last class of methods are based on the construction of a probability distribution on the input domain which, given a set of elements to cover w. r. t. some coverage criteria, maximises the weakest probability for an element to be activated by an execution. For instance, structural statistical testing based on the "all-instructions" coverage criteria leads to the construction of an input distribution which avoid too weak probability for a statement to be exercised, even if this statement is only used for a small subset of the input domain. Similarly, "all-branches", "all-paths¾n", or any other structural coverage criteria can be used as a basis for structural statistical testing. This is a way to combine random testing and coverage requirements, no element in the set to be covered being seldom or never exercised during testing.
We present a new way of automating structural statistical testing using the CS package for counting and randomly generating combinatorial structures. This tool is part of the MuPAD system. Uniform generation of so-called "labelled combinatorial structures" has been studied for the average case complexity analysis of algorithms by Flajolet et al., and implemented in CS by Denise et al.: this analysis requires counting all the possible input cases of a given size and considering a uniform probability distribution on them.
It turns out that execution paths in control graphs can be modelled by such structures. Thus CS provides a way of drawing uniformly from the paths of a given length of a program.
Moreover, we show how to use it for other sets of paths, for instance those of length less than a given bound, those passing through a specific node or edge of the graph. This make possible to cope with coverage criteria such as "all-instructions" or "all-branches".
Reference:
S.-D. Gouraud, A. Denise, M.-C. Gaudel, B. Marre. A New Way of Automating Statistical Testing Methods. In Proc. 16th Int. Conf. on Automated Software Engineering, IEEE, Coronado Island, 26-29 Nov. 2001, pp. 5-12.
Tom Maibaum (tom@maibaum.org, tom@dcs.kcl.ac.uk),
Aspassia Daskalopulu (aspassia@dcs.kcl.ac.uk)
Department of Computer Science, King's College London, The Strand, London WC2R 2LS, UKTheo Dimitrakos (t.dimitrakos@rl.ac.uk)
CLRC Rutherford Appleton Laboratory, Oxfordshire, OX11 0QX, UK
One aspect of the development of e-market services for the facilitation of business-to-business electronic commerce concerns the provision of automated support for contract performance. Assessing the parties' performance of an agreement, once it comes into force, requires reasoning with the contract terms (obligations, rights, powers and other legal relations that obtain between parties) as they go about conducting their business exchange, sometimes complying and sometimes deviating from their pre-agreed prescribed behaviour. Compliance with prescribed behaviour is typically evaluated individually by each partner to an agreement and where parties' views differ, disputes arise that require some form of resolution.
In this paper we present a simple architecture for an e-market, where an artificial (controller) agent undertakes such resolution. The controller's decision-making is informed by the agreement and each party's view of whether its own and the counter-party's behaviour comply with it. Thus, the controller forms an opinion on the basis of such evidence (and possible additional recommendations from agents representing the parties), in similar spirit to a (human) judge's process of reasoning in arriving at her ruling. We consider this as a belief formation problem and explore the potential of using subjective reasoning to represent an individual's (possibly partial) views and to reason about their joint conflict and consensus formation. We comment on the relation of such belief formation on the establishment of trust between partners to an agreement and between the latter and the controller of an e-market.
The aim of graph transformation is - as the aim of algebraic specification - the formal modeling of data processing systems in a systematic way. While the central semantic entity of algebraic specification is a data type, i.e. an algebra with operations on data domains, graph transformation yields binary relations on graphs, which are syntacttically described by rules and control conditions.
In the talk, a survey of GRACE, a GRAph- and rule-CEntered approach to system modeling is given. The development of GRACE involves researches from Berlin, Bremen, Erlangen, Munich, Oldenburg and Paderborn. The main goals are:
See http://www.informatik.uni-bremen.de/theorie for more details.
References
Marc Andries, Gregor Engels, Annegret Habel, Berthold Hoffmann, Hans-Jörg Kreowski, Sabine Kuske, Detlef Plump, Andy Schürr, Gabriele Taentzer: Graph Transformation for Specification and Programming. Science of Computer Programming 34:1-54, 1999.
Frank Drewes, Peter Knirsch, Hans-Jörg Kreowski, Sabine Kuske: Graph Transformation Modules and Their Composition. In M. Nagl, A. Münch, M. Schürr (Eds.), Proc. Applications of Graph Transformations with Industrial Relevance (AGTIVE'99), volume 1779 of Lecture Notes in Computer Science, pages 15-30. Springer, 2000.
Sabine Kuske: More about control conditions for transformation units. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, Grzegorz Rozenberg (Eds.), Proc. Theory and Application of Graph Transformations, volume 1764 of Lecture Notes in Computer Science, pages 323-337. 2000.
Sabine Kuske: Transformation Units--A structuring Principle for Graph Transformation Systems. PhD thesis, University of Bremen, 2000.
Hans-Jörg Kreowski, Sabine Kuske: Graph Transformation Units and Modules. In Hartmut Ehrig, Gregor Engels, Hans-Jörg Kreowski, Grzegorz Rozenberg (Eds.), Handbook of Graph Grammars and Computing by Graph Transformation, Vol. 2: Applications, Languages and Tools, pages 607-638. World Scientific, Singapore, 1999.
Hans-Jörg Kreowski, Sabine Kuske: Graph Transformation Units with Interleaving Semantics. Formal Aspects of Computing 11:690-723, 1999.
Hans-Jörg Kreowski, Sabine Kuske, Andy Schürr: Nested graph transformation units. International Journal on Software Engineering and Knowledge Engineering 7:479-502, 1997.
J.L.Fiadeiro ATX Software and University of LisbonWhereas, together with inheritance, feature calling - the basic mechanism of object-oriented computation - has helped developers in taming the complexity of constructing new systems, the challenge today is on evolution, namely on endowing system components with agility in responding to change and dynamically procuring collaborations from which global properties of the system can emerge. Because a feature call applies a specific feature of a specific class to a specific instance of that class, interactions in object-oriented systems are too tightly coupled and rigid to support the levels of agility that are required to operate in business environments that are "time critical", namely those that make use of Web Services, B2B, P2P or operate in what is known as "internet-time". We claim that an alternative approach can be found in what we call "coordination technologies" - a set of analysis techniques, modelling primitives, design principles and patterns that we have been developing for externalising interactions into explicit, first-class entities that can be dynamically superposed over system components to coordinate their joint behaviour.
More information can be obtained from http://www.atxsoftware.com/.
joint work withA semantics for architectural specifications in CASL is discussed, with special attention paid to an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for CASL models. To circumvent this problem, we extend the CASL logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL. In the specific framework of the CASL institution, we also discuss a calculus for discharging the static amalgamation conditions. These are in general undecidable, but can be dealt with by approximative algorithms in all practically relevant cases.Lutz Schroeder, Till Mossakowski, Piotr Hoffman, Bartek Klin
Based on the following papers:
Schroeder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.
Semantics of architectural specifications in CASL.Schroeder, L., Mossakowski, T., Tarlecki, A.
IN: Proc. 2nd Conf. on Foundamental Aspects of Software Engineering FASE'01, ETAPS'2001, Genova, April 2001, H. Hussman, ed., Lecture Notes in Computer Science 2029, 253-266, Springer-Verlag 2001.
Amalgamation in CASL via enriched signatures.Klin, B., Hoffman, P., Tarlecki, A., Schroeder, L., Mossakowski, T.
In: Proc. 28th Intl. Coll. on Automata, Languages and Programming ICALP'01, F. Orejas, P. Spirakis, J. van Leeuwen, eds., Lecture Notes in Computer Science 2076, 993-1004, Springer-Verlag 2001.
Checking Amalgamability Conditions for CASL Architectural Specifications.
In: Proc. 26th Intl. Symp. Mathematical Foundations of Computer Science MFCS'01, J. Sgall, A. Pultr, eds., Lecture Notes in Computer Science 2136, 451-463, Springer-Verlag 2001.
For the specification of large software systems, heterogeneous multi-logic specifications are needed, since complex problems have different aspects that are best specified in different logics. Heterogeneous specification allows formal interoperability among languages and tools.
In the literature, several approaches to heterogeneous specification have been developed. They deal with the integration of different logics via logic projections, logic encodings and bridges of proof calculi. We show how to combine these approaches into a single, simplified approach. Proof support for this setting can be obtained from the proof calculus for development graphs with hiding.
Paper and slides are available from http://www.tzi.de/~till/publications.html
Abstract missing
The talk first introduces the B specification method. B belongs to model-oriented specification methods [Abr96]. Data specification relies upon Set Theory, static and invariant properties are written in First-Order Logic and actions (operations) are described by predicate transformers. A specification unit is called a "machine" which encapsulates a state and provides exported operations. A machine can be refined by another kind of unit called "refinement". The last refinement in a development chain is called an "implementation". These units must fulfill syntactic conditions. For example, operations in implementations must be fully deterministic. Moreover, it is possible to combine machines by the way of aggregating links "includes" and "uses". A complex development can be split in a structured way by means of "imports" and "sees" primitives. Validation conditions (called proof obligations) ensures that operations preserve the invariant of the state and that a refinement preserves the observable effect of the machine (or the refinement) that it refines.
Event systems are an extension of the formalism that allow the user to specify systems evolving by means of "events". The events may be triggered only if their guard is true. The theoretical framework of Event-B is the same as the one of classical B. Nevertheless, refinement conditions are more flexible because they allow introduction of new events which are not present (or not perceptible) at a more abstract level. So, it is admitted that Event-B is more powerful than classical B from a user point of view. For a presentation of Event-B, see for example [AM98].
The second part of the talk is devoted to the presentation of the construction of finite labelled transition systems (LTS) from B abstract systems [BC00]. This work is done in our team to investigate the benefits of a (sometimes partial) representation of the behaviour of B event systems. We choose to decompose the state of an abstract system in several disjunctive predicates. These predicates provide the basis for defining a set of states which are the nodes of the LTS, while the events are the transitions. We illustrate the method by developing the SCSI-2 (Small Computer Systems Interface) input-output system. We intend to carry out a connection between the B environment (Atelier B) and the Caesar/Aldebaran Development Package (CADP) which is able to deal with finite LTS.
[Abr96] J.-R. Abrial, The B Book - Assigning Programs to Meanings. Cambridge University Press, 1996.
[AM98] J.-R. Abrial and L. Mussat, Introducing Dynamic Constraints in B. In Recent Advances in the Development and Use of the B Method, p. 83-128, Proc of the 2nd Int. B Conf., LNCS 1393, Springer-Verlag, 1998.
[BC00] D. Bert and F. Cave, Construction of Finite Labelled Transition Systems from B Abstract Systems. In Integrated Formal Methods, p. 235-254, Proc. of the 2nd Int. Conf. IFM2000, LNCS 1945, Springer-Verlag, 2000.
Modular Operational Semantics is a recently-developed variant of Plotkin's original Structural Operational Semantics (which subsumes Kahn et al.'s Natural Semantics). It has several advantages over the original framework:
The foundations of Modular Operational Semantics involve Labelled Transition Systems where the configurations are just abstract syntax (enriched by allowing nodes to be replaced by their computed values), and where all auxiliary entities are incorporated as components of labels on transitions. The set of labels naturally forms an (indexed) product category, and the labels on successive transitions in computations are required to trace paths through this category. The identity morphisms of the category provide a built-in notion of unobservable label. Surprisingly, this particular combination of the familiar notions of Labelled Transition System and Category does not appear to have been exploited elsewhere.
The advantages of Modular Operational Semantics over conventional Structural Operational Semantics have been demonstrated in a description of Concurrent ML, and in a specification of the Action Notation used in Action Semantics. Some papers on these topics, as well as on the foundations of the new framework, are available at: http://www.brics.dk/~pdm/ModularSOS.html.
Comments are welcome!
Reports on recent activities at Member sites are to be added here.
| | | Abstracts of Talks |