An industrial application of symbolic model checking

Model checking techniques are recognized to provide reliable and copious results. Instead of examining a few cases only – as it is done in testing – model checking includes the whole state space in mathematical proofs of correctness. Yet, this completeness is seen as a drawback as the state explosion problem is hard to handle. In our industrial case study, we apply automated model checking techniques to an innovative elevator system, the TWIN by ThyssenKrupp. By means of abstraction and nondeterminism, we cope with runtime behaviour and achieve to efficiently prove our specification’s validity. The elevator’s safety requirements are exhaustively expressed in temporal logic along with real-world and algorithmic prerequisites, consistency properties, and fairness constraints. Beyond verifying system safety for an actual installation, our case study demonstrates the rewarding applicability of model checking at an industrial scale. CR subject classification  D.2.4; F.3.1; J.7 ; C.3     

Animations-Framework in Java Systematische Animationsentwicklung mit Mehrschichtenarchitektur

Multimedia-Anwendungen und Animationen sind durch Dynamik gekennzeichnet. Die Dynamik muss sich in der Architektur der Anwendung niederschlagen. Eine M?glichkeit hierbei besteht darin, die Dynamik in einer speziellen Softwareschicht innerhalb einer Mehrschichtenarchitektur zu realisieren. Dieses Papier stellt ein Animations-Framework in Java vor, das diese Architektur JavaBeans-konform als muster-orientiertes Framework realisiert und somit die systematische Entwicklung von animierten Multimedia-Anwendungen in Java unterstützt.     

Das AutoMoDe-Projekt Modellbasierte Entwicklung softwareintensiver Systeme im Automobil

Die Entwicklung eingebetteter Software für Automobile ist inh?rent komplex und vereint verschiedene Entwicklungsphasen, mehrere fachliche Disziplinen, sowie verschiedene Akteure in beteiligten Unternehmen. Der AutoMoDe-Ansatz zur Entwicklung automotiver Software beschreibt Systeme auf verschiedenen Abstraktionsebenen und definiert schrittweise überg?nge zwischen diesen Ebenen. Neben der Definition geeigneter Ebenen werden zur Modellierung von Echtzeitsystemen ein einheitliches Berechnungsmodell sowie dom?nenspezifische Beschreibungstechniken verwendet. Automatisierte Anbindungen für Analyse und Synthese komplexer Softwaresysteme mit dem Ziel eines konsistenzbetonten Entwicklungsprozesses wurden realisiert. Die beschriebenen Techniken wurden in den Werkzeugprototypen AutoFocus integriert und im Zusammenspiel mit einer Werkzeugkette demonstriert.     

Rekonstruktion von Software-Architekturen Ein Literatur- und Methoden-überblick zum Stand der Wissenschaft

Software-Architekturen werden aus verschiedenen Sichten beschrieben, die abh?ngig von den Anliegen sind, die mit der Beschreibung verfolgt werden. In vielen F?llen ist die Software-Architektur eines Systems nicht ausreichend beschrieben. Sichten müssen dann rekonstruiert werden, um für Planung von ?nderungen zur Verfügung zu stehen. Dieser Artikel fasst die in der wissenschaftlichen Literatur vorgeschlagenen Techniken zur Rekonstruktion von Software-Architektursichten zusammen und stellt sie den Sichten des Architekturentwurfs gegenüber. Anhand der Gegenüberstellung identifiziert er Forschungsbedarf.     

Die Beweisentwicklungsumgebung W\Omega -Mkrp

Zusammenfassung. Die Beweisentwicklungsumgebung -Mkrpsoll Mathematiker bei einer ihrer Hauptt?tigkeiten, n?mlich dem Beweisen mathematischer Theoreme unterstützen. Diese Unterstützung mu? so komfortabel sein, da? die rechnergestützte Suche nach formalen Beweisen leichter und insbesondere weniger aufwendig ist, als ohne das System. Dazu mu? die verwendete Objektsprache ausdrucksstark sein, man mu? die M?glichkeit haben, abstrakt über Beweispl?ne zu reden, die gefundenen Beweise müssen in einer am Menschen orientierte Form pr?sentiert werden und vor allem mu? eine effiziente Unterstützung beim Füllen von Beweislücken zur Verfügung stehen. Das im folgenden vorgestellte $\Omega$-Mkrp-System ist der Versuch einer Synthese der Ans?tze des vollautomatischen, des interaktiven und des planbasierten Beweisens. Dieser Artikel soll eine übersicht über unsere Arbeit an diesem System geben. Eingegangen am 24. Juni 1994 / Angenommen am 3. November 1995     

Lesetechniken für die Inspektion von Software-Anforderungsdokumenten Ein kontrolliertes Experiment zur Untersuchung der Effektivit?t und Verwendung von Zeit bei der Anwendung verschiedener Lesetechniken

Inspektion hilft bereits in frühen Phasen der Softwareentwicklung, die Qualit?t von Softwareprodukten zu bestimmen und Nachbearbeitungsaufwand einzusparen. Lesetechniken sind ein Ansatz, der die Aufmerksamkeit von Inspektoren beim individuellen Lesen auf bestimmte Fehlermengen lenken und dadurch die Arbeit mehrerer Inspektoren untereinander koordinieren soll. Diese Arbeit berichtet über ein Experiment, das einerseits die Effektivit?t und Effizienz mehrerer Lesetechniken auf individueller und auf Teamebene miteinander vergleicht und andererseits Zusammenh?nge der Verwendung von Lesezeit mit der Effektivit?t von bestimmten Inspektorengruppen untersucht.     

Formale objektorientierte Softwareentwicklung mit FOX{\cal F}{{\scriptstyle{\cal O}{\cal X}}}

Zusammenfassung.   Wir stellen die neue Methode vor, die auf die formale Entwicklung sequentieller, objektorientierter Softwaresysteme abzielt. ist eine synergetische Kombination aus der semiformalen Methode Fusion und der formalen Spezifikationssprache Object-Z. Die Methode unterscheidet ausdrücklich Analyse und Entwurf, um die Komplexit?t und die unterschiedlichen Aufgaben der Softwareentwicklung zu bew?ltigen. In jeder Entwicklungsphase werden Zustands- und Verhaltensspezifikationen in graphischer oder textueller Form erstellt. Wir geben Beweisverpflichtungen an, um zu gew?hrleisten, da? die entwickelten Spezifikationen formal konsistent und vollst?ndig sind, und da? das resultierende System zur Ausgangsspezifikation konform ist. Wir illustrieren die Anwendung von an einem einfachen Beispiel, einem Grapheditor. Eingegangen am 24. Dezember 1996 / Angenommen am 8.10.1997     

Personalization in the public sector: An inventory of organizational and user obstacles towards personalization of electronic services in the public sector

The public sector more and more deploys personalized e-government services. Personalization offers great opportunities to make communication more effective and efficient, to infer and predict citizens' behavior and to even influence behavior. However, some drawbacks must be considered. Important organizational barriers hinder the implementation of personalized e-government services and important user obstacles, such as access, trust, control, and privacy, have to be overcome to make fruitful use of those personalized e-government services.