We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence “While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career.” We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how formal methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these. In this article, we aim at highlighting why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the tradeoffs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly supported by formal methods.

A calculus for the specification and verification of distributed concurrent interactive real-time systems is introduced. Systems are specified by their interface behavior formalized by interface predicates and interface assertions. System designs in terms of architectures of distributed networks of interactive systems are constructed by concurrent composition of subsystems. The specification of system designs is calculated from the specifications of their subsystems. Verification is done by proof rules, which are based on the concepts of causality and realizability justified by the operational model in terms of generalized Moore machines, Moore machines not restricted to finite state spaces. The calculus supports interface specification and reasoning both about untimed as well as timed distributed concurrent systems. This includes the design of cyber-physical systems. Real-time is used, in particular, to specify time-sensitive behavior and to prove properties related to causality and realizability, properties that hold for all Moore machines. On this basis, a calculus is worked out and illustrated by small examples. The calculus is shown to be sound and relatively complete.

Background: During the last decades, the functional power and complexity of automotive E/E architectures grew radically and is going to grow further in the future. For highly and fully automated driving, functions with the highest safety integrity level need to be realized, requiring new development methodologies and a new level of formal rigor. Aim: We investigate to what extent SOA concepts are applicable for safety-critical embedded automotive software systems and whether this concept is appealing to E/E architects. Method: We conducted a survey research by interviewing system architects at our industrial partner, then we applied the grounded theory method in order to derive a theory and a set of requirements for an automotive SOA approach. Additionally, we illustrate the approach using a function needed in a highly automated driving scenario. Results: We present a formal service model and an automotive SOA framework. Both aspects, i.e., architecture structuring and formal service description resulted from the analyzed interview data. Limitation: This approach has not been evaluated extensively, yet. Conclusion: Our first results suggest that SOA concepts are indeed successfully applicable in (continuous) automotive software engineering and are a means to cope with complexity and safety requirements.

Cyber-Physical Systems require more advanced modeling techniques to capture physicality including time and space, reliability in terms of probabilistic models, connectivity in terms of communication links, adaptivity, context awareness, interoperability, and autonomy. This requires a comprehensive integrated modeling framework for specification, modeling of architecture, and tracing their relationships.

Automotive architectures today consist of up to 100 electronic control units (ECUs) that communicate via one or more FlexRay and CAN buses. Multiple control applications - like cruise control, brake control, etc. are specified as Simulink/Stateflow models, from which code is generated and mapped onto the different ECUs. In addition, scheduling policies and parameters, both for the ECUs and the buses, need to be specified. Code generation/optimization from the Simulink/Stateflow models, task partitioning and mapping decisions, as well as the parameters chosen for the schedulers all of these impact the execution times and timing behaviour of the control tasks and control messages. These in turn affect control performance, such as stability and steady-/transient-state behaviour. This paper discusses different aspects of this multi-layered design flow and the associated research challenges. The emphasis is on model-based code generation, analysis, testing and verification of control software for automotive architectures, as well as on architecture or platform configuration to ensure that the required control performance requirements are satisfied.

Product line engineering dealing with software and system families for automotive systems needs a deeper structuring and understanding of systems, their functions, and operational modes than the engineering of individual systems, since the variability of the systems introduces an additional dimension and further complexity. In fact, the enormous complexity of systems today requires a much more structured approach to engineering anyhow. It will be demonstrated how to derive a better structuring of systems by three complementary views at the conceptual level including 1) the context view in terms of context models, 2) the functional view by function hierarchies and operational modes 3) component architecture models. These views bridge the gap between functional requirements and their technical realization. We show how such an approach leads to a more structured understanding of systems in terms of different views on their properties and their mutual logical relation and how this can be used as a basis for product line engineering. We introduce concepts, in particular, of logic to define logical dependencies between different levels of abstractions and perspectives of systems.

A theory for the systematic development of distributed interactive software systems constructed in terms of components requires a basic system model and description techniques supporting specific views and abstractions of systems. Typical system views are the interface, the distribution, or the state transition view. We show how to represent these views by mathematics and logics. The development of systems consists in working out these views leading step by step to implementations in terms of sets of distributed, concurrent, interacting state machines. For large systems, the development is carried out by refinement through several levels of abstraction. We formalize the typical steps of the development process and express and justify them directly in logic. In particular, we treat three types of refinement steps: horizontal refinement which stays within one level of abstraction, vertical refinement addressing the transition from one level of abstraction to another, and implementation by glass box refinement. We introduce refinement relations to capture these three dimensions of the development space. We derive verification rules for the refinement steps and show the modularity of the approach.

More than 20 years of research has created a large body of ideas, concepts, and theories for model-based development of embedded software-intensive systems. These approaches have been implemented by several tools and successfully applied to various development projects. However, the everyday use of model-based approaches in the automotive and avionic industries is still limited. Most of the time, the engineers work with a predefined set of isolated tools, and therefore adapt their engineering methods and process to the available tools. Today, the industry achieves tool integration by demand-driven, pragmatic, and ad-hoc composed chains of a priori existent commercial tools. Nevertheless, these tool chains are not (and cannot be) seamless, since the integration that can be achieved is not deep enough. This hampers the reuse and refinement of models, which subsequently leads to problems like redundancy, inconsistency, and lack of automation. In the end, these deficiencies decrease both the productivity and quality that could be provided by model-based approaches. To overcome these problems, a deep, coherent, and comprehensive integration of models and tools is required. Such an integration can be achieved by the following three ingredients: 1) a comprehensive modeling theory that serves as a semantic domain for the models, 2) an integrated architectural model that holistically describes the product and process, and 3) a manner to build tools that conform to the modeling theory and allow the authoring of the product model. We show that from a scientific point of view, all ingredients are at our hands to do a substantial step into an integrated process and tool world. Further, we illustrate why such a solution has not been achieved so far, and discuss what is to be done to get a step closer to seamless model-based engineering.

Provides an overview of the technical articles and features presented in this issue.

Some of the distinct attributes of Aerospace and Automobile Software Technologies are briefly reviewed in this article as a way of placing in collective-context the detailed technical papers that form this exciting special issue. A historical context, a unifying architectural perspective and, the rapidly changing and defining role of software is presented, especially as we look ahead to this new decade in this still young century.

In the development of embedded systems starting from high-level requirements and going over to system specification and further to architecture various aspects and issues have to be elicited, collected, analyzed and documented. These start from early phase contents like goals and high level requirements and go on to more concrete requirements and finally to system specifications, architecture design documents on which the final implementation of the system is based.

Global software engineering has become a fact in many companies due to real necessity in practice. In contrast to co-located projects global projects face a number of additional software engineering challenges. Among them quality management has become much more difficult and schedule and budget overruns can be observed more often. Compared to co-located projects global software engineering is even more challenging due to the need for integration of different cultures, different languages, and different time zones-across companies, and across countries. The diversity of development locations on several levels seriously endangers an effective and goal-oriented progress of projects. In this position paper we discuss reasons for global development, sketch settings for distribution and views of orchestration of dislocated companies in a global project that can be seen as a ldquovirtual project environmentrdquo. We also present a collection of questions, which we consider relevant for global software engineering. The questions motivate further discussion to derive a research agenda in global software engineering.

No abstract available.

Abstract Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.

We introduce a theory for the identification, modeling, and formalization of two methodologically essential, complementary views onto software and software intensive systems. One view addresses mainly tasks in requirements engineering when describing the overall system functionality from the users' point of view. By this view we aim at the specification of the comprehensive user functionalities of multifunctional systems in terms of their functions, features, and services as well as their mutual dependencies. This view leads to a function or service hierarchy. The other view essentially addresses the design phase with its task to develop logical architectures formed by networks of cooperating components that are specified by their interface behavior.

The amount of software in cars grows exponentially. Driving forces of this development are the availability of cheaper and more powerful hardware, as well as the demand for innovation through new functionality. The rapidly growing significance of software and software-based functionality is at the root of various challenges in the automotive industries. These concern their organization, definition of key competencies, processes, methods, tools, models, product structures, division of labor, logistics, maintenance, and long-term strategies. This paper pinpoints the idiosyncrasies of the domain, characterizes the essentials of automotive software, and discusses the challenges of automotive software engineering

Service-oriented software systems rapidly gain importance across application domains: They emphasize functionality (services), rather structural entities (components), as the basic building block for system composition. More specifically, services coordinate the interplay of components to accomplish specific tasks. In this article, we establish a foundation of service orientation: Based on the Focus theory of distributed systems (see Broy and Stølen [2001]), we introduce a theory and formal model of services. In Focus, systems are composed of interacting components. A component is atotalbehavior. We introduce a formal model of services where, in contrast, a service is apartialbehavior. For services and components, we work out foundational specification techniques and outline methodological development steps. We show how services can be structured and how software architectures can be composed of services and components. Although our emphasis is on a theoretical foundation of the notion of services, we demonstrate utility of the concepts we introduce by means of a running example from the automotive domain.

The amount of software in cars grows exponentially. Driving forces of this development are cheaper and more powerful hardware and the demand for innovations by new functions. The rapid increase of software and software based functionality brings various challenges (see [21], [23], [25], [26]) for the automotive industries, for their organization, key competencies, processes, methods, tools, models, product structures, division of work, logistics, maintenance, and long term strategies. From a software engineering perspective, the automotive industry is an ideal and fascinating application domain for advanced techniques. Although the automotive industry may adopt general results and solutions from the software engineering body of knowledge gained in other domains, the specific constraints and domain specific requirements in the automotive industry ask for individual solutions and bring various challenges for automotive software engineering. In cars we find literally all interesting problems and challenging issues of software and systems engineering.

Information technology has become the driving force of innovation in many areas of technology and, in particular, in the form of embedded systems in vehicles. Embedded hardware/software systems control innovative functions in cars, support and assist the driver and realize new features for information and entertainment. A rapid development brought more and more digital hardware and software into a modern car only within little more than two decades. Systems and software engineering for embedded systems in vehicles is today one of the great scientific, methodological, and technical challenges. In modern cars we find all issues of software systems in a nutshell. This brings a wide spectrum of challenges for the automotive industry, including business, management, and technical issues. In the following we outline the main problems, research challenges and approaches to deal with them.

Abstract. Today, component-based software and system development has gained considerable attention and is wide-spread. Components and/or modules manifest the well-proven engineering principle of divide and conquer. Formal approaches have helped to provide a theoretical foundation to component-orientation. There is a broad range of system architectures in practice today in terms of layered distributed open systems (as for example known in telecommunications). However, the mathematical formalisms developed so far are rarely applied to these practical architectures. In fact, the notion of distribution and stacked communication layers is hardly understood precisely and not supported by architecture description languages. This article addresses this gap. The formal conditions of distribution and layering are investigated and a mathematical model for layered distributed systems is presented. Communication refinement and so-called complex connectors turn out to be vital concepts which are not addressed in today’s modeling languages. In addition to that, two important design approaches are derived for the architectural design of complex communication systems: A node-centric and a network-centric design approach. Both can significantly improve the design process.

EHAVIOR models play a key role in the engineering of software-basedsystems.Theyarethebasisforsystematic approaches to requirements elicitation, specification, architecture design, simulation, code generation, and verification and validation. A range of notations, techniques, and tools supporting behavior modeling for these development tasks have been suggested. Underlying these notations, techniques, and tools, two complementary approaches to modeling behavior can be identified: interaction-based and state-based modeling. Interaction-based modeling focuses on the interactions between actors and components in a system. Consequently, communication between such entities is viewed as the principal modeling construct. Interaction modeling, commonly realized using scenario and use case techniques, provides an overall view of a system which is particularly suited for supporting communication between project

Technical systems of today often include large amounts of embedded software. Today, in general, embedded software offers various functionalities, is distributed over networks and structured into logical components that interact. To understand and develop software-intensive systems we need fundamental models of multi-functional software system combining services and composed of concurrently interacting components forming architectures. We need methods to specify system properties, identify and describe various basic views onto systems, and show how they are related. We consider, in particular, models of data, functionality, states, interfaces, interaction, hierarchical composed systems, and processes. We study relationships by abstraction and refinement as well as forms of composition and modularity. In particular, we introduce a comprehensive mathematical model for composed systems, their views and their relationships as needed in a comprehensive development process. Finally we outline a consequent architecture-centered model driven development process.

No abstract available.

Information technology has become the driving force of innovation in many areas of technology and also in cars. Embedded software controls the functions of cars, supports and assists the driver and realizes systems for information and entertainment. Software in automobiles is today one of the great challenges for software engineering. On modem cars we find all issues of software systems in a nutshell. It is a challenge for software and systems engineering.

Today, in general, software is embedded, distributed onto networks and structured into logical components that interact asynchronously. We study fundamental models of composed software systems and their properties, identify and describe various basic views, and show how they are related. We concentrate on models of composed systems that interact by message exchange. We consider, in particular, models of data, states, interfaces, hierarchical composed systems, and processes. We study relationships by abstraction and refinement as well as forms of composition and modularity. In particular, we introduce a comprehensive mathematical model for composed systems, its views and their relationships.

No abstract available.

The definition of a transparent software architecture is one of the key issues in the early development phases for complex distributed and reactive software systems. In this paper, we show how to derive an architecture systematically for systems with communication models based on broadcasting. Adequate graphical description techniques for capturing interaction requirements and logical component architectures for broadcasting systems are unavailable so far. We introduce an extension to UML's sequence diagrams to capture broadcasting scenarios. Furthermore, we present methodological steps for constructively deriving structural and behavioral aspects of the architecture under consideration from the captured scenarios.

The development of large software systems consists of a sequence of modeling tasks. It requires the modeling and description of the application domain, software requirements, software architecture, software components, their internal structure, and their implementation. Technically, in software engineering, we work with a development method and description techniques with modeling, refinement, and implementation concepts. Today, much of the modeling is carried out by informal text and graphical description techniques. The development is organized in a development process and supported by CASE tools. We show how mathematics can provide a scientific foundation for the modeling aspects, description techniques, and development methods of software engineering. Such a scientific foundation leads to a deeper understanding of the development process and to a basis for a more powerful tool support.

We adapt the Dijkstra/Scholten calculational logic to partial functions in a way that preserves the fixed point rule.

We introduce the formal notion of an interaction interface. Its purpose is to specify formally the interaction between two or more components that co-operate as subsystems of a distributed system. We suggest the use of interaction interfaces for the description not of the behaviour of a single component in isolation but of the interface, the co-operation, between two or more components that are interacting within a distributed system. Typical examples are the interaction between an embedded system and its environment or the interaction between a sender and a receiver in a communication protocol. An interaction interface can be formally described by predicates characterising sets of interaction histories. We understand the specification of interaction histories as a typical step in system development that prepares the decomposition of a system into interacting subcomponents. After fixing the distribution structure of the system, an interaction interface is worked out that describes how the introduced subcomponents interact. In a successive development step we systematically derive the individual component specifications from the interface description. We show how such an interaction interface can be decomposed systematically into component specifications.

A crucial aspect of the architecture of a software system is its decomposition into components and the specification of component interactions. In this report we use a variant of extended event traces as a graphical technique for the description of such component interactions. It allows us to define interaction patterns that occur frequently within an architecture, in the form of diagrams. The diagrams may be instantiated in various contexts, thus allowing reuse of interaction patterns. Our notation contains operators yielding not only exemplary but complete behavior specifications. Extended event traces have a clear semantics that is based on sets of traces. We present several application examples that demonstrate the practical use of our notation.

We introduce a method to describe systems and their components by functional specification techniques. We define notions of interface and interaction refinement for interactive systems and their components. These notions of refinement allow us to change both the syntactic (the number of channels and sorts of messages at the channels) and the semantic interface (causality flow between messages and interaction granularity) of an interactive system component. We prove that these notions of refinement are compositional with respect to sequential and parallel composition of system components, communication feedback and recursive declarations of system components. According to these proofs, refinements of networks can be accomplished in a modular way by refining their compponents. We generalize the notions of refinement to refining contexts. Finally, full abstraction for specifications is defined, and compositionality with respect to this abstraction is shown, too.

The paper studies the incorporation of a fair nondeterministic choice operator into a generalization of Dijkstra's calculus of guarded commands. The generalization drops the law of the excluded miracle to allow commands that correspond to partial relations. Because of fairness, the new operator is not monotonic for the orderings that are generally used for proving the existence of least fixed points for recursive definitions. To prove the existence of fixed points it is necessary to consider several orderings at once, and to restrict the class of recursive definitions.

A formal model and a logical framework for the functional specification of time-sensitive communicating systems and their interacting components are outlined. The specification method is modular with respect to sequential composition, parallel composition, and communication feedback. Nondeterminism is included by underspecification. The application of the specification method to timed communicating functions is demonstrated. Abstractions from time are studied. In particular, a rational is given for the chosen concepts of the functional specification technique. The relationship between system models based on nondeterminism and system models based on explicit time notions is investigated. Forms of reasoning are considered. The alternating bit protocol is used as a running example.

Abstract Some extensions of the basic formalism of stream processing functions are useful to specify complex structures such as operating systems. In this paper we give the foundations of higher order stream processing functions. These are functions which send and accept not only messages representing atomic data, but also complex elements such as functions. Some special notations are introduced for the specification and manipulation of such functions. A representation of time is outlined, which enables us to model time dependent behaviour. Finally, we demonstrate how characteristic operating system structures can be modelled by timed higher order stream processing functions.

Abstract A formal model is described for the CCITT specification and description language SDL which provides a graphical concept for representing designs of systems interacting by signals. The model is based on functional descriptions of interactive systems using the concept of streams and stream processing functions. The foundations for this functional modelling of interactive systems are introduced. The graphical constructs of SDL are related to this model. In particular it is shown how the meaning of SDL graphical forms can be represented by specifications in the form of conditional equations or by functional programs. Based on the functional formal model the application of specification and verification methods for SDL is demonstrated. Small examples are treated. A number of tools are discussed that can be based on that model. This study does not define a semantic model for the specification and design language SDL, but it gives An introduction to the functional modelling of distributed systems An explanation of how to translate SDL designs into functional descriptions An extended example for the translation of an SDL design A discussion of the possibilities of supporting SDL designs by such a semantic foundation

A simple programming language for the description of networks of loosely coupled, communicating, nondeterministic agents is introduced. Two possible graphical interpretations are discussed: finite cyclic and infinite acyclic, tree-like graphs. Operational semantics for such graphs is defined by computation sequences. The merge anomaly is described, analysed and explained. Two fixed-point semantics are defined in a denotational style, one that avoids the merge anomaly, and another one that includes the merge anomaly, and they are proved to be consistent with the resp. operational definitions. Both definitions are compared and analysed.

Starting from an algebraic specification of the data type QUEUE several variants of communicating agents representing queues are studied. It is demonstrated how new issues such as exceptions, robustness, and concurrency can be considered, when going from a purely algebraic view of queues to queues used in the framework of communicating systems. Nevertheless the verification of the communicating agents can be done by classical techniques for proving implementations correct, developed in the framework of algebraic specification. Finally the design of infinite networks representing queues and their verification is demonstrated. Although shown only for a simple example a general method is aimed at for the development of interactive and concurrent programs from algebraic specification using applicative programming styles.

The algebraic specification of the semantics of programming languages is outlined. Particular emphasis is given to the problem of specifying least-fixed points by first-order conditional equations. To cover this issue, the theory of specifying partial heterogeneous algebras by abstract data types is slightly extended by a more general notion of homomorphism. In this framework the semantics of programming languages can be uniquely specified in a purely algebraic way, using particular models of a hierarchy of abstract types. This approach is demonstrated for a simple procedural programming language. Several increasingly complex versions of iterations are treated and analyzed with respect to their theoretical consequences. Finally, as a complementary algebraic technique, transformational semantics is explained and applied to our examples.

An applicative language is introduced for representing concurrent programs and communicating systems in the form of mutually recursive systems of nondeterministic equations for functions and streams. Mathematical semantics is defined by associating particular fixed points with such systems. These fixed points are chosen using a combination of several complete partial orderings. Operational semantics is described in the form of term rewriting rules, consistent with the mathematical semantics. It represents data-driven reduction semantics for usual expressions and data-driven data flow semantics in the case of recursive stream equations. So the language allows to treat the basic semantic notions of nondeterminism, parallelism, communication, and concurrency for multiprogramming in a completely formal, applicative framework. In particular, it provides a semantic theory for networks of loosely coupled, nondeterministic, communicating, stream processing functions. Finally, the relationship of the presented language to partial recursive functions and nonconventional computational models such as data flow and reduction machines is shown.

The basic idea of the Schorr-Waite graph-marking algorithm can be precisely formulated, explained, and verified in a completely applicative (functional) programming style.Graphs are specified algebraically as objects of an abstract data type.When formulating recursive programs over such types, one can combine algebraic and algorithmic reasoning: An applicative depth-first-search algorithm is derived from a mathematical specification by applying properties of reflexive, transitive closures of relations.This program is then transformed in several steps into a fmal procedural version with the help of both algebraic properties of graphs and algorithmic properties reflected in the recursion structure of the program.

A methodology of program development by transformations is outlined. In particular, ways of representing the transformation rules are discussed, and the relationship between notions of their correctness and the semantic definition of programming languages is studied. How transformation techniques are complemented by the use of abstract data types and assertions is described. In the resulting calculus of transformations, the single rules not only represent design or optimization techniques, but they also incorporate verification principles. To illustrate this approach, the Warshall algorithm is developed by successive applications of transformations.

Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.