Abstracts of Talks

Abstracts of Talks

Reiko Heckel: Consistency-Preserving Model Evolution Through Transformations

Reiko Heckel with Gregor Engels and Jochen M. Küster,
University of Paderborn, Germany
Luuk Groenewegen,
Leiden University, The Netherlands

With model-based development being on the verge of becoming an industrial standard, the topic of research of statically checking the consistency of a model made up of several submodels has already received increasing attention. The evolution of models within software engineering requires support for incremental consistency analysis techniques of a new version of the model after evolution, thereby avoiding a complete reiteration of all consistency tests.

In this paper, we discuss the problem of preserving consistency within model-based evolution focusing on UML-RT models. We introduce the concept of a model transformation rule that captures an evolution step. Composition of several evolution steps leads to a complex evolution of a model. For each evolution step, we study the effects on the consistency of the overall model and provide localized consistency checks for those parts of the model that have changed. For a complex evolution of a model, consistency can then be established by incrementally performing those localized consistency checks associated to the transformation rules applied within the evolution.

The work has been reported on in a paper presented at the UML 2002 in Dresden [http://www.uni-paderborn.de/cs/ag-engels/Papers/2002/EngelsHKG-UML02.pdf].

Slides: http://www.uni-paderborn.de/cs/ag-engels/Talks/2002/Heckel-UML02.pdf

Dominique Duval: A zooming process for building specifications

Dominique Duval, Christian Lair, Catherine Oriat, and Jean-Claude Reynaud

The far specification S is very simple, however its interpretation may be wrong. On the contrary, the near specification U is complex, but its interpretation is right. The zooming process builds an INTERMEDIATE specification T, which is both simple and right. However, the issue is that T is not a specification in the usual (e.g. algebraic) sense. In the context of diagrammatic specifications, as introduced in [DL02], the three specifications S, T and U are of the same nature, and the description of the zooming process is quite simple. The running example in this talk deals with the treatment of an error.

Reference:

[DL02]. D. Duval, C. Lair. Diagrammatic Specifications. Rapport de recherche IMAG-LMC 1043 (2002). An improved version, with extended bibliography, is submitted for publication. http://www-lmc.imag.fr/lmc-cf/Dominique.Duval/publisinfo.html

Keywords: Categorical semantics of formal languages, Sketches and generalizations, Abstract data types and algebraic specification.

Michel Bidoit: On the Integration of Observability and Reachability Concepts

Michel Bidoit and Rolf Hennicker

Paper: Michel Bidoit and Rolf Hennicker. On the integration of observability and reachability concepts. In Proc. 5th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS'2002), Grenoble, France, Apr. 2002, volume 2303 of Lecture Notes in Computer Science, pages 21-36. Springer, 2002.

http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2002-2.rr.ps

Martin Hofmann: Static prediction of heap space usage of first-order functional programs

Martin Hofmann and Steffen Jost
LMU Muenchen

Our analysis is not restricted to linearly typed functional programs but requires a semantic condition for nonlinear ones which states that only the last of multiple uses of the same variable may be modifying. This semantic condition is formulated with respect to a standard operational semantics and can be guaranteed by a number of existing analyses and type systems.

We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management.

The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions.

Grigore Rosu: On Lightweight Formal Methods in System Specification and Verification

Grigore Rosu

The traditional methods to verify software systems are model checking and theorem proving. These methods are quite general and offer increased confidence in the correctness of a program once "proved" correct, but, unfortunately, due to state explosion or lemma discovery, they do not always scale up well and are often unusable in practical situations, even after significant efforts in abstraction and architectural/functional decomposition. Instead of exploring methods for showing full correctness of programs, searching therefore for all the errors in a program at the expense of intractability, we rather focus on techniques that find many errors efficiently. More precisely, we present uses of algebraic specification in what we call domain-specific certification and runtime verification; the former is concerned with showing statically that a program does not violate basic safety policies of the domain under consideration (for example, that one does not add meters and seconds), while the later is concerned with finding requirements violations during testing and/or enforcing correct behavior during operation.

Proving correctness of programs, in addition to difficulties in stating the problem rigorously and in trusting compilers, is known to be undecidable even for simple programming languages. Fortunately, due to increased safety measures and enormous resources invested in validation of flying software, NASA's software is relatively clean and well documented and its programmers are often willing to insert formal annotations in the code. Additionally, much of NASA's software is developed for specific domains, such as astronomical navigation, and many errors are of specific kinds related to these domains, such as subtraction of two vectors that are not represented in the same coordinate frame. Domain-specific certification is the process of showing automatically that a program does not have a "specific to a domain" type of errors.

A domain-specific certifier consists of three main components: 1) an algebraic specification of an abstract domain of interest; 2) a syntax (specification) of a programming language of interest enriched with domain-specific annotations; and 3) an algebraic specification defining a domain-specific abstraction of programming language constructs (instructions or blocks) into the abstract domain. We have implemented and experimented with three domain specific certifiers so far, all having a segment of C as programming language. One is for measurement units, checking programs for unit inconsistencies, such as addition of values having incompatible units. Another one is for astronomical navigation, certifying that operations on vectors, such as addition, subtraction, and rotation, are effectuated consistently. Using this domain-specific certifier, we have found a non-obvious error in Amphion, an astronomical navigation program synthesis tool. The third is for state estimation software and certifies that a program is a proper Kalman Filter calculating an optimum estimate of a state. All these certifiers need annotations in the code, relating the programming language variables to their meaning in the abstract domain, and are totally automatic. Their abstract domains are specified using hundreds of axioms. The third additionally requires the user to insert proofs of optimality together with the Kalman Filter code, in a proof-carrying code style; due to the limited number of known and accepted Kalman Filters, these proofs can be reused.

The first two certifiers are very efficient, analyzing more than 1000 lines of code per second, while the third takes about 30s to certify 100,000 proof steps. All our specifications use membership equational logic (MEL) and are implemented in Maude, which is a high performance executable specification language. Our third certifier additionally uses ITP, an inductive theorem prover implemented in Maude, to check the proof scripts inserted in the code as annotations; these proofs of optimality are very complex and are usually 4-5 orders of magnitude larger than the code.

The tools and techniques above assume that programs are not concurrent. Concurrency adds significant complexity to program verification, due to the exponential number of possible interleavings. Model checking is the standard technique to verify concurrent programs, showing that any possible execution satisfies the (usually temporal logic) specification, but it is often too slow to be used in practice. Full correctness of a program implies indeed correct execution, but what is important, after all, is the latter. Runtime verification is the process of monitoring/enforcing a formal requirements specification at execution time. The executing program is instrumented to emit events to an observer, which checks them against the specification. We are developing a runtime verification tool, called PathExplorer (PaX), which has already found multiple errors in a Mars rover software larger than 35,000 lines of C code. The observer of PaX uses membership equational and rewriting logics as implemented in Maude, as meta-languages to specify and implement monitoring logics. We have experimented so far with temporal logics, whose efficient implementation in Maude is able to monitor 100 million events in 2 minutes.

The slides of this talk can be found at http://www-faculty.cs.uiuc.edu/~grosu/download/ifipWG13.ppt

Mark D. Ryan: Structuring systems by features

Mark D. Ryan

I start by reviewing some known examples of feature integration and feature interaction. Then I describe the approach taken in our project funded by British Telecom and EPSRC, which consists of defining a new language construct for defining features, and the case studies we have examined.

I describe the logical properties of the feature construct for SMV, and show that it satisfies the postulates of theory update.

Further information:

http://www.cs.bham.ac.uk/~mdr/research/projects/01-fc/index.html

ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/00-scp.ps.gz http://www.cs.bham.ac.uk/~heh/ecai02.pdf

Special Joint Session with the AGILE project on Mobility

---

Hubert Baumeister: (UML) Extensions for Mobility

Hubert Baumeister

In this talk I present the research that has been done at the University of Munich with respect to mobilty within the AGILE project. The AGILE project is an EU funded project within the Global Computing Initiative to study architectures for mobility [2].

Nora Koch, Piotr Kosiuczenko, Martin Wirsing, and myself are working on extensions of UML activity diagrams for mobility [3]. First, we provide stereotypes to model mobile objects, locations, and activities like moving or cloning. Then, we present two notational variants of activity diagrams for modeling mobility. One variant is location centered and focuses on the topology of locations. The other one focuses on the actor responsible for an activity.

Piotr Kosiuczenko is working on an extension of UML sequence diagrams for mobility [4]. He models the behaviour of mobile objects using a generalized version of lifelines. For different kinds of actions like creating, entering or leaving a mobile object stereotyped messages are used. Kosiuczenko provides also a zoom-out, zoom-in facility to allow him to abstract from specification details.

Finally, Stephan Merz and Júlia Zappe have defined a spatio-temporal logic for the specification and analysis of the behaviour of mobile systems [5]. This logic is based Lamport's TLA and extends it by providing operators to describe properties of tree and changes in their structure.

In the presentation, a common example, the airport case-study, is used to illustrate the different approaches.

References:

[1] Slides of the presentation: http://www.informatik.uni-muenchen.de/~baumeist/slides/agile-ifip02.pdf

[2] AGILE Web-site: http://www.pst.informatik.uni-muenchen.de/projekte/agile/

[3] Baumeister, Hubert and Koch, Nora and Kosiuczenko, Piotr and Wirsing, Martin. Extending Activity Diagrams to Model Mobile Systems, to appear in in proceedings Net.Objects Days. 2002
http://www.informatik.uni-muenchen.de/~baumeist/publications/actdiagmob.pdf

[4] Kosiuczenko, Piotr. Sequence Diagrams for Mobility (New Version), S. Spaccapietra(ed): Proc. of 21 International Conference on Conceptual Modeling, ER'02, Tampere, Finland, LNCS, Springer, Berlin, 2002 (to appear)
http://www.pst.informatik.uni-muenchen.de/~kosiucze/SDM.pdf

[5] Zappe, Júlia: Towards A Mobile TLA. ESSLLI 2002: 14th European Summer School in Logic, Language and Information, Trento, Italy, 2002. Proceedings to the ESSLLI 2002 Student Sessions.
http://www.pst.informatik.uni-muenchen.de/~zappe/papers/esslli02.ps.gz

---

Antonia Lopes: Coordination for Mobility: the airport case study

Antonia Lopes (joint work with José Luiz Fiadeiro)

With the advent of mobile computing in wide and ad-hoc networks, new forms of distributed systems come about. For these systems, distribution is a third dimension that, together with computation and coordination, needs to be taken into account at an architectural level of design. In this talk, we present our first steps towards the goal of having an architectural approach to distribution and mobility: the addition of this new dimension to the architectural framework that we developed in the past (centred on CommUnity). Moreover, we use the airport case study to illustrate that the resulting architectural approach supports the externalization and explicit representation of the distribution aspects of systems in architectural designs.

The slides are available at

http://www.di.fc.ul.pt/~mal/papers/agile&ifip.pdf

---

Diego Latella: On Mobility Extensions of UML Statechart Behaviours. A Pragmatic Approach

Diego Latella and Mieke Massink
CNR/ISTI, Pisa, Italy

In this talk a simple extension of a behavioural subset of UML Statecharts in order to deal with mobility issues is proposed. The extension builds on the notion of Multicharts, as proposed in [GLM01]. A Multichart is a collection of Statecharts, each Statechart being associated with its unique input queue. In a Multichart each Statechart can address its output events directly to each (other) Statechart of the Multichart by explicitly mentioning the name of (the unique queue of) such Statechart in its send actions.

The first, obvious, extension we propose in the present work allows the use of (queue) name variables in send actions, which implies the extension of the global statechart status with the inclusion of a binding function. This way the destination of a send-action is not statically fixed although Statecharts still cannot select the partners from which to receive events. The resulting asymmetric communication paradigm is well suited for object-based/oriented systems.

The second extension consists in relaxing the unique association between each Statechart and its input-queue. Now, a Multichart is composed by a collection of Statecharts and a shared pool of queues, the Multiqueue. The specification of the trigger event in the transitions in the Statecharts is enriched with the explicit indication of the queue from which the trigger input event is to be received. Such indication can also be done via a (queue name) variable, thus allowing for the dynamic evolution of the interconnection structure between the Statecharts of the Multichart. The resulting communication paradigm is much more flexible than the asymmetric one and is well suited for mobility-oriented as well as fault tolerant systems.

In the paper the formal semantics for both extensions is given, following a similar style as in [LMM99,GLM01a]. The relationship between input-queue selection and stuttering is addressed as well.

Work of ours on the behavioural subset of UML Statecharts (UMLSDs) related to what presented at the talk includes:

• An initial formal semantics for UMLSDs [LMM99]
• LTL model checking of UMLSDs [LMM00]
• ACTL model checking of UMLSDs [GLM01]
• Stochastic Time extension of UMLSDs [GLM00]
• Testing Theory for UMLSDs [LaM01]
• Conformance Testing for UMLSDs [LaM02, GLM03]

References

[GLM00] S.Gnesi, D.Latella, and M.Massink.
A stochastic extension of a behavioural subset of UML statechart diagrams.
In L.Palagi and R.Bilof, editors, Fifth IEEE International High-Assurance Systems Engineering Symposium, pages 55-64. IEEE Computer Society Press, 2000. ISBN 0-7695-0927-4.

[GLM01] S.Gnesi, D.Latella, and M.Massink.
Modular semantics for a UML Statechart Diagrams kernel and its extension to Multicharts and Branching Time Model Checking
The Journal of Logic and Algebraic Programming. Elsevier Science, 51(1):43-75, 2002

[GLM03] S.Gnesi, D.Latella, and M.Massink.
Formal Conformance Testing of UML Statechart Diagrams Behaviours
(submitted)

[LMM00] D.Latella, I.Majzik, and M.Massink.
Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker.
Formal Aspects of Computing. The International Journal of Formal Methods. Springer-Verlag, 11(6):637-664, 1999.

[LMM99] D.Latella, I.Majzik, and M.Massink
Towards a formal operational semantics of UML statechart diagrams.
In P.Ciancarini, A.Fantechi, and R.Gorrieri, editors, IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Oriented Distributed Systems, pages 331-347. Kluwer Academic Publishers, 1999. ISBN 0-7923-8429-6.

[LaM01] D.Latella and M.Massink.
A formal testing framework for UML Statechart Diagrams behaviours: >From theory to automatic verification.
In A.Jacobs, editor, Sixth IEEE International High-Assurance Systems Engineering Symposium, pages 11-22. IEEE Computer Society Press, 2001. ISBN 0-7695-1275-5.

[LaM02] D.Latella and M.Massink. On testing and conformance relations of UML Statechart Diagrams Behaviours.
In P.G. Frankl, editor, Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis, pages 144-153. Association for Computing Machinery - ACM, 2002. ACM Software Engineering Notes 27(4), ISBN 1-58113-562-9.

---

Michele Loreti: A Klaim specification of the handover protocol: logic-based and type-based analisys

Michele Loreti and Daniele Gorla

We present two analysis techniques developed for Klaim, an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities, code mobility and distribution, and remote asynchronous communication.

The first analysis technique is a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic and the mu-calculus, but has novel features that permit dealing with state properties to describe the effect of actions over the different sites. To avoid that full knowledge of implementation details is required when establishing nets properties, we have also introduced a framework for specifying contexts for Klaim nets and for guaranteing that, under given assumptions, specific properties are satisfied, regardless of the concrete realizations. This permits guaranteeing formula satisfaction along with progressive substitution of parts of the context (i.e. under­specified components) with concrete nets (i.e. fully implemented components).

The second analysis technique is a type system to control resource access in a setting where access rights can be acquired and lost, both by fixed and mobile entities (i.e. Klaim nodes and agents). Because of this highly dynamic nature of policies, we were forced to rely on run-time type checking of programs, or part of them. Indeed, static verification is useful in many circumstances since it avoids the use of expensive dynamic mechanisms, however it is hardly sufficient in the Internet context. To deal with open systems (i.e. systems whose structure can change dynamically in unpredictable ways), dynamic type checking is needed, e.g. mobile agents are dynamically type checked at run-time when they migrate. Moreover, we extended this framework to grant different privileges to processes coming from different nodes and to constraint the operations allowed over different kinds of data (thus, e.g., preventing dangerous operations over specific sensible data). We finally present the implementation in Klaim of the Handover protocol, an example of handling dynamic reconfigurations of a wireless net, namely the mobile phones network. In this setting, we show how to use our techniques to prove a number of significant logical and security properties.

The papers, presenting full details of our works, are available at http://music.dsi.unifi.it.

The slides of the talk can be found at http://music.dsi.unifi.it/presentations/agilechiemsee.ppt.

Narciso Marti-Oliet: Executing SOS specifications in Maude

Narciso Marti-Oliet and Alberto Verdejo

Although a rewriting logic representation of the CCS semantics was given previously, it cannot be directly executed in the current default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by exploiting the reflective properties of rewriting logic, which allow controlling the rewriting process.

Then we show how to bridge the gap between theory and practice in a new implementation of the CCS operational semantics in Maude, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2.0. Comparing this implementation with the previous one, we think that it is not only much more efficient but also much closer to the mathematical presentation of the CCS semantics, that is, the representational distance has been greatly reduced.

In both cases, we show how the semantics can be extended to traces of actions and to the CCS weak transition relation where internal actions are not observed, and on top of them we implement the Hennessy-Milner modal logic for describing processes.

These ideas have been extended to make them applicable to the more complex Full LOTOS language, where in addition user-defined datatypes have to be integrated, and also (in the Maude 2.0 version) to the operational semantics and may testing equivalence of an asynchronous version of the pi-calculus, where the binding constructs are handled by means of the CINNI calculus of explicit substitutions.

Related papers and Maude code can be retrieved from http://dalila.sip.ucm.es/~alberto/esf/

Tom Maibaum: A Logical Basis for the Specification of Reconfigurable Component-Based Systems

Tom Maibaum (joint work with Nazareno Aguirre)

Special specification languages, called architecture description languages (ADLs), were proposed to describe and analyse properties of (sometimes evolving) architectures. Many of these are able to deal with what is called dynamic reconfiguration, i.e., with the description of operations which may modify the system's structure at run time. While ADLs provide constructs for modelling the architecture of a system, they often do not support a language for reasoning about possible system evolution. In other words, ADLs support the definition of components, interconnections and transformation rules or operations for making architectures evolve, but any kind of reasoning about behaviours is often performed in some "meta-language", sometimes informally. Moreover, architectural elements in ADLs are usually described operationally, as opposed to declaratively.

We wish, then, to be able to specify and reason about the consequences of using certain reconfiguration operations in a declarative manner, adding abstraction to what, to our understanding, can be operationally specified by ADLs.

We adapt a logic proposed by Manna and Pnueli for the specification of reactive systems for this purpose. We present the logic and some results that make it suitable for the specification of dynamically reconfigurable systems. A language based on this logic is defined, where systems specifications are hierarchically organised around the following notions:

• the notion of components, which are represented by classes that define templates for these components;
• the notion of connector type, which we call associations, which are then used to define the potential ways in which components may be organised in a system;
• the notion of subsystem, the new notion that defines the unit of modularity from which reconfigurable systems are built, and which conveys the information about what components, what associations and what reconfiguration operations are used to define the module.

A characterisation of the inheritance relationship between component definitions is also proposed. Inheritance is defined in terms of (restricted) theories extentions, which seems to correspond to a natural interpretation of inheritance, and allows for the use of polymorphism within subsystems.

Papers and more info: http://www.dcs.kcl.ac.uk/staff/aguirre/index.html

Till Mossakowski: Heterogeneous proofs - the local and the global view

Till Mossakowski

Compared with logic combination, heterogeneous specification (and proofs) has only weaker forms of feature interaction, but is easier, more flexible and wider applicable (one metaformalism for all logics), and supports better re-use of existing proof tools (no need to implement new calculi).

The slogan is: heterogeneous specification is structured specification over the Grothendieck institution, formed over an arbitrary but fixed graph of institutions and institution comorphisms. The restriction to comorphisms is justified elsewhere (see my WADT 2002 talk about Foundations of heterogeneous CASL).

For institution-independent proofs in structured specifications, we use the formalism of development graphs. These admit an easy formulation of a global calculus (using normal form signatures, while keeping the structure). The effect is that the Craig interpolation property (needed in Borzyszkowski's more local calculus) is not needed here.

Proofs in the heterogeneous framework now can be obtained in different ways. The first possibility is to globally encode the Grothendieck institution into a "universal" logic being rich enough and coming with good tool support (e.g. HOL). Such a global encoding can be obtained by a coherent set of local encodings of the individual logics. Via heterogeneous borrowing, we can reduce heterogeneous proving to structured proving in the "universal" logic.

The second, more local, possibility is to have a whole set L of tool-supported logics, such that each logic is encoded into some logic in L. We can then use borrowing into some logic in this set. This enables us to use more specialized tool support, depending on the particular proof goal. This approach needs structured proving in the Grothendieck institution.

Now the calculus for structured proving mentioned above needs weak amalgamation of the institution as a prerequisite. Hence, the problem is to obtain weak amalgamation for the Grothendieck logic. A theorem by Diaconescu guarantees this under the assumptions that all individual institutions, all institution comorphisms and the institution indexing admit amalgamation. (Diaconsecu also needs left-adjointness of signature translations because he works with morphisms.)

However, these assumptions do not hold in practice: some institutions like CASL do not admit (weak) amalgamation, nor do comorphisms from CASL to HOL. The institution indexing in many cases is not even cocomplete.

Hence, we propose a different approach. We work with weakly amalgamable cocones instead of colimits and require weak amalgamation only for the above mentioned subset L of the institutions. The comorphisms and the indexing only need to admit weak amalgamation. We do not need preservation of colimits, since we are working with weakly amalgamable cocones only. For the indexing, this means that there is some "rich, but not that big" encoding-maximal institution like HOL.

With these assupmtions, we do not obtain weak amalgamation for the Grothendieck institution, but we still obtain a sound and relatively complete proof calculus for heterogeneous proofs. "Relatively" here means relative to oracles deciding conservativeness of extensions in logics from L.

We give a sample heterogeneous proof involving modal logic and first-order logic. The main proof goal is split into two subgoals, one of which is entirely within propositional modal logic, while the other one is within first-order logic. The subgoals can then be discharged using tools for the individual logics.

The slides are available under http://www.informatik.uni-bremen.de/~till/papers/ifip02.pdf

Peter Padawitz: Interactive Computation and Proof with Expander2

Peter Padawitz
peter.padawitz@udo.edu
University of Dortmund
Germany

Expander was written in ML. Expander2 has been implemented in O'Haskell [2], an extension of Haskell [1] with object-oriented features for reactive programming and a typed interface to Tcl/Tk for developing GUIs. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, to admit several degrees of interaction and to keep the system open for extensions or adaptations of individual components to changing demands.

Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types [3][4][5]. Swinging types combine constructor-based visible types with state-based hidden types and have unique (Herbrand) models, which interpret relations as the least or greatest solutions of their axioms.

[9] provides slides of the talk. [8] concentrates on the prover capabilities of Expander2. All features of the system and their use are described in the manual [7], which also contains installation guidelines.

 [1]

P. Hudak, J. Peterson, J.H. Fasel, A Gentle Introduction to Haskell 98, www.haskell.org/tutorial, Yale and Los Alamos 2000

 [2]

M.P. Jones, J. Nordlander, B. v. Sydow, M. Carlsson, A Survey of O'Haskell, http://www.cs.chalmers.se/~nordland/ohaskell/survey.html, 2001

 [3]

P. Padawitz, Proof in Flat Specifications, in E. Astesiano, H.-J. Kreowski, B. Krieg-Brückner, eds., Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Report, Springer 1999

 [4]

P. Padawitz, Swinging Types = Functions + Relations + Transition Systems, Theoretical Computer Science 243 (2000) 93-165

 [5]

P. Padawitz, The Swinging World, http://ls5-www.cs.uni-dortmund.de/~peter/Swinging.html

 [6]

P. Padawitz, Expander: A System for Testing and Verifying Functional-Logic Programs, http://ls5-www.cs.uni-dortmund.de/~peter/Expander.html

 [7]

P. Padawitz, Expander2: A Formal Methods Presenter and Animator, http://ls5-www.cs.uni-dortmund.de/~peter/Expander2/Expander2.ps and http://ls5-www.cs.uni-dortmund.de/~peter/Expander2/Expander2.html

 [8]

P.Padawitz, Expander2: Towards a Workbench for Interactive Formal Reasoning, FM TOOLS 2002, http://ls5-www.cs.uni-dortmund.de/~peter/Chiemsee.ps.gz

 [9]

P.Padawitz, Interactive Computation and Proof with Expander2: Slides, http://ls5-www.cs.uni-dortmund.de/~peter/ChiemseeSlides.ps.gz

Joseph Goguen: Conditional Circular Coinductive Rewriting

Joseph Goguen, Kai Lin, and Grigore Rosu
Dept. Computer Science & Engineering, Univ. California, San Diego
Department of Computer Science, University of Illinois, Urbana-Champaign

A natural extension of algebraic specification splits sorts into visible for data and hidden for states, and defines states to be behaviorally equivalent iff they are indistinguishable under all visible valued contexts. While standard many sorted equational proof techniques like induction are suitable for the visible part, coinduction or context induction is usually needed to prove non-obvious behavioral equivalences. Unfortunately, these methods can require intensive human intervention, and hence are unsuitable for complex problems. We know only three languages that support automated behavioral reasoning, Spike, CafeOBJ and BOBJ; the first uses context induction, and the other two use coinduction. Behavioral satisfaction is computationally harder than equational satisfaction; more precisely, it is Pi₂⁰-hard, so no algorthim can prove [or disprove] all behaviorally true [or false] statements.

CCRW and CCCRW are implemented in BOBJ, and they take as input a behavioral specification and a hidden sorted equation, returning true or false, or else looping forever; CCRW has been in BOBJ for several years. The talk illustrated it on a some non-trivial (infinite) stream examples, showing in particular the automatic generation of cobases, and the automatic generation of circular coinductive lemmata.

CCRW works well in practice because the circularities contain variables, which can be instantiated with appropriate substitutions for reuse. Although theorems of constants and of deduction ("implication elimination") hold for behavioral satisfaction, this approach is unsuitable for proving conditional behavioral equations because it yields ground equational proof obligations. CCCRW generalizes CCRW to conditional equations, without using these theorems, and appears to be the most powerful automated proof technique now available for behavioral equivalence. The talk described it in detail and gave examples of its use, showing details of its computation.

The talk finally discussed case analysis, which we found is often required for larger applications. BOBJ provides linguistic support for case analysis can which can drastically reduce the size of proofs. Case definitions in BOBJ are first class citizens, that can be named, reused, and combined with other such definitions.

The full paper will prove correctness of the CCCRW algorithm, and give examples showing some of its limitations. It will also prove correctness of the extension of rewriting, and hence of CCCRW, to handle case analyses.

URL for the slides:

http://www.cs.ucsd.edu/users/goguen/pps/cccrwsl.ps

Dirk Pattinson: What's a proof by Coinduction, semantically?

Dirk Pattinson

If the underlying endofunctor T is accessible, final models arise as limits of the so-called terminal sequence (Tⁿ 1), where 1 = { 0 } is a one element set and n ranges over ordinal numbers. This allows us to extract a proof principle by looking at the projections p_n: C -> Tⁿ 1 from (carriers of) T-coalgebras into the objects of the terminal sequence: We show that two points c, d are behaviorally equivalent if and only if the projections p_n(c) and p_n(d) coincide for all ordinals less than the accessibility degree of the underlying endofunctor. This proof principle, which we call "terminal sequence induction" enables us to use (transfinite, but otherwise ordinary) induction to establish behavioral equivalences.

This proof principle is then applied in two different settings: First, we show how terminal sequence induction can be used to obtain properties of co-recursively defined functions, allowing for short and elegant proofs. As second application, we re-prove Moss' expressivity theorem coalgebraic logic. We believe that our proof is considerably simpler and conceptually clearer than the original proof given by Moss.

Abstracts of Talks