Abstract:

Abstract:This Festschrift contains papers written by friends, students and colleagues to honor Manfred Broy in celebration of his 60th birthday. It presents results in the area of systems and software engineering - Manfred's research area - comprising both theoretical and practical aspects. The Festschrift is divided into two volumes. The first volume contains ten scientific contributions and presents results for the more foundational issues of Manfred's research area ranging from formal verification and specification to concurrency and formal transformation. The second volume comprises seven papers and is devoted to more practical aspects of systems and software engineering. It presents interesting approaches to model-driven, automated, and change-driven software development and discusses issues in feature-oriented modeling, abstraction patterns and framework construction. The papers of both volumes have a clear relation with Manfred's research; some of them even compare or extend Manfred's work, and all papers contain personal notes of the authors where they explain there relationship with Manfred ...

Abstract:How Euclid might have written and checked the correctness of his famous algorithm had he been a little further ahead of his time.

Abstract:In his article Experience with Software Specification and Verification Using LP, the Larch Proof Assistant, Manfred Broy verified (as one of his smaller case studies) the Majority Vote Algorithm by Boyer and Moore. LP requires that all user theories are expressed axiomatically. I reworked the example in Isabelle/HOL and turned it into a definitional development, thus proving its consistency. In the end, a short alternative proof is given.

Abstract:Specification of interactive distributed systems has been a challenge for decades. We present an overview of the specification techniques for these systems based on dataflow networks and stream processing. It covers models of streams and specification of stream processing systems that are related to and based on the development method Focus invented by Manfred Broy and his group. We introduce a basic set of manipulator operations for streams, stream bundles, stream processing functions, and give a summary of related state-based specification techniques. Furthermore we sketch an overview of implementations for the Focus framework. These range from formalizations using interactive proof assistants and model checkers to the modeling IDE AutoFocus.

Abstract:The Logic of Partial Functions (LPF) is used to reason about propositions that include terms that can fail to denote values: this paper provides two semantic descriptions for LPF. A Structural Operational Semantics (SOS) gives an intuitive introduction; this is followed by a denotational semantics where relations are chosen for denotations offering an intuitive model of undefined terms. Finally, we illustrate how the denotational semantics can be used as a basis for proofs about propositions that include terms that can fail to denote.

Abstract:A theory, graphical notation, mathematical calculus and implementation for finding whether two given expressions can, at execution time, denote references attached to the same object. Intended as the seed for a comprehensive solution to the "frame problem" and as an alternative (for the specific issue of determining aliases) to separation logic, shape analysis, ownership types and dynamic frames.

Abstract:We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect.

Abstract:In this paper we present a method based on UML sequence diagrams for integrating policy requirements with requirements to system design and functionality in the development process. The approach allows policy requirements to be taken into account throughout the system development instead of in a post hoc manner. The method supports the formalization of system specifications and policy specifications at various levels of abstraction, where the abstraction levels are related by refinement. The notion of policy adherence formally captures what it means that a system specification satisfies a policy specification. For analysis with respect to adherence at abstract levels to be meaningful, the results must be preserved under refinement. This paper gives a characterization of conditions under which adherence is preserved under refinement, and identifies development rules that guarantee adherence preservation. By results of transitivity and modularity, the development process, as well as analysis tasks, may be conducted in a stepwise manner addressing individual parts of the specifications separately.

Abstract:Mondex electronic purses are used to replace cash payment by electronic payment with a smart card. Tool-based proofs of an abstract specification of the security protocol used by Mondex cards has been proposed as a challenge for mechanized verification. This paper extends the challenge and describes a comprehensive formal approach for developing Mondex that starts with the abstract specification that was used to certify Mondex, and ends with correct Java code. The development was verified with the theorem prover KIV using several refinements. Mondex cards can also be viewed as a challenge for software engineering a security-critical application. We describe a model-driven tool-supported approach, that uses UML models enhanced with security aspects, and generates correct and secure Java Card code. The UML models can also be used to generate the formal specifications used in KIV.

Abstract:Structural aspects play a key role in the model-driven development of software systems. Effective techniques and tools must therefore be based on suitable representation formalisms that facilitate the specification, manipulation and analysis of the structure of models. Graphical and algebraic approaches have been shown to be very successful for such purposes: 1) graphs offer natural a representation of topological structures, 2) algebras offer a natural representation of compositional structures, 3) both graphs and algebras can be manipulated in a declarative way by means of rule-based techniques, 4) they allow for a layered presentation of models that enables compositional techniques and favours scalability. Most of the existing approaches represent such layering in a plain manner by overlapping the intra- and the inter-layered structure. It has been shown that some layering structures can be conveniently represented by an explicit hierarchical structure enabling then structurally inductive manipulations of the resulting models. Moreover, providing an inductive presentation of the structure facilitates the compositional analysis and verification of models. In this paper we compare and reconcile some recent approaches and synthesise them into an algebraic and graph-based formalism for representing and manipulating models with inductively defined hierarchical structure.

Abstract:Algebraic High-Level (AHL) nets are defined as integration of Petri nets with algebraic data types, which allows to model the communication structure and the dataflow within one modelling framework. Transformations of AHL-nets -- inspired by the theory of graph transformations -- allow in addition to modify the communication structure. More- over, high-level processes of AHL-nets capture the concurrent semantics of AHL-nets in an adequate way. Altogether we obtain a powerful integrated formal specification technique to model and analyse all kinds of communication based systes. In this paper, we give a comprehensive introduction of this framework -- including main results concerning parallel independence of AHL-transformations and amalgamation of processes -- and show how this can be applied to model and analyse modern communication and collaboration platforms like Google Wave and Wikis. Especially we show how the Local Church-Rosser theorem for AHL-net transformations can be applied to ensure the consistent integration of different platform evolutions. Moreover the amalgamation theorem for AHL-processes shows under which conditions we can amalgamate waves of different Google Wave platforms in a compositional way.