Verifying of interface assertions for infinite state Mealy machines

This paper aims at techniques and methods for the verification of logical assertions about the interface behavior of generalized I/O-state machines. The interface behavior of such machines is specified by interface assertions formulated in predicate logic. Interface assertions specify the interface behavior of state machines in terms of the streams of messages produced via their input and output channels. The verification of interface assertions for state machines is carried out with the help of generalized invariants. Such invariants are proved for state machines in terms of stable assertions. Nontrivial liveness properties such as fairness lead to specifications and also to state machines defining sets of computations that specify sets of output streams that are not limit closed. Elementary examples for such cases are described and the implied complications are analyzed. Furthermore, verification methods are provided for these cases and demonstrated by small examples.     

Systemorientiertes Automotive Engineering

Zusammenfassung  Die Zunahme der durch Informations- und Kommunikationstechnologien erbrachten Funktionalit?ten in Automobilen stellt die Industrie vor neue Herausforderungen. Weitergehende Anforderungen zur Individualisierung, und damit zur Modell- und Variantenvielfalt, sowie der Zwang zu schnellen Modellwechseln bedingen eine steigende Komplexit?t, spezifische Kostenstrukturen und eine weitergehende Arbeitsteilung bei optimierter Produktivit?t in Entwicklung und Produktion. Dies und der wachsende Kostendruck sind der Hintergrund, vor dem das essenzielle Wechselspiel zwischen der Vielzahl der Funktionen und Systeme im Rahmen immer kürzerer Innovationszyklen beherrscht werden muss. Die dazu notwendige Zusammenarbeit unterschiedlicher Disziplinen wie Informatik und Informationstechnik mit traditionellen Ingenieurdisziplinen wie Maschinenbau und Elektrotechnik, erfordert zwingend die Herausbildung eines ganzheitlichen systemorientierten Automotive Engineerings.     

The 'Grand Challenge' in Informatics: Engineering Software-Intensive Systems

The science of information and information processing, informatics comprises many areas and includes principles of computing, storing, communicating, and visualizing information, and formalisms to describe information-processing procedures. The development and production of information-processing systems is based on software support systems such as software tools or product data repositories. Software and systems engineering is thus the key discipline for constructing information-processing systems. In particular, software and systems engineering addresses issues such as requirements engineering, architectural design, implementation, reliability engineering, and long-term maintenance. Developing a methodology for specifying and verifying software-intensive systems poses a grand challenge that a broad stream of research must address     

Ein Wegweiser für Forschung und Lehre im Software-Engineering eingebetteter Systeme

Bisher wurde das Gebiet der Software für eingebettete Systeme („embedded systems”) von der Informatik zu wenig beachtet.     

Multifunctional software systems: Structured modeling and specification of functional requirements

This paper deals with the structured specification of interface behavior of multifunctional systems, which are systems that offer a variety of functions for different purposes and use cases. It introduces a theory and first concepts of a methodology for the identification, structured modeling, and formalization of functional requirements of multifunctional systems. Service hierarchies specify multifunctional systems in terms of their provided sub-functions called services together with their mutual relationships and dependencies. A service hierarchy describes the functionality of multifunctional systems in a structured way. Each service is specified independently and the specification is added to the service hierarchy. Modes help to specify the feature interactions and by that functional dependencies between the services. The approach is based on the Focus theory for modeling interface behavior and services.