Sicherheitskritische Eingebettete Systeme
2018

[inproceedings] bibtexW. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, und A. Rakow, "Using Traffic Sequence Charts for the Development of HAVs.
@inproceedings{conf/ERTS/DKMPR2018,
author = {Werner Damm and Stephanie Kemper and Eike Möhlmann and Thomas Peikenkamp and Astrid Rakow},
title = {{Using Traffic Sequence Charts for the Development of HAVs}},
booktitle = {Embedded Real Time Software and Systems  ERTS2018},
note = {submitted},
year = {2018},
month = {February},
}
2017

[article] bibtexW. Damm und R. Kalmar, "Autonome Systeme  Fähigkeiten und Anforderungen, pp. 400408
@ARTICLE{,
author = {Damm, W. and Kalmar, Ralf},
title = {Autonome Systeme  F{\"{a}}higkeiten und Anforderungen},
journal = {InformatikSpektrum},
number = {Vol. 40, No. 5. Berlin Heidelberg: SpringerVerlag},
year = {2017},
pages = {400408},
issn = {1432122X},
doi = {10.1007/s0028701710630} } 
[article] bibtexW. Damm und P. Heidl, "SafeTRANS Working Group: Highly automated Systems:Test, Safety, and Development Processes
@ARTICLE{,
author = {Damm, Werner and Heidl, Peter},
title = {SafeTRANS Working Group: Highly automated Systems:Test, Safety, and Development Processes},
journal = {Recommendations on Actions and Research Challenges},
year = {2017},
abstract = {The Management Summary summarizes regulatory and research challenges to be addressed for costeffective safe deployment of highly automated systems with excellent quality. The focus is on the overall development process, including architecture and security aspects, as well as verification and validation (V & V).} } 
[inproceedings] bibtexE. Böde, M. Büker, W. Damm, G. Ehmen, M. Franzle, S. Gerwinn, T. Goodfellow, K. Grüttner, B. Josko, B. Koopmann, T. Peikenkamp, F. Poppen, P. Reinkemeier, M. Siegel, und I. Stierand, "Design Paradigms for MultiLayer Time Coherency in ADAS and Automated Driving (MULTIC).
@INPROCEEDINGS{multic_final_report,
author = {B{\"{o}}de, E. and B{\"{u}}ker, M. and Damm, W. and Ehmen, G. and Franzle, M. and Gerwinn, S. and Goodfellow, T. and Gr{\"{u}}ttner, K. and Josko, B. and Koopmann, B. and Peikenkamp, T. and Poppen, F. and Reinkemeier, P. and Siegel, M. and Stierand, I.},
month = {October},
title = {{Design Paradigms for MultiLayer Time Coherency in ADAS and Automated Driving (MULTIC)}},
booktitle = {FAT Series},
number = {302},
year = {2017},
note = {Available online at \url{https://www.vda.de/en/services/Publications/fatschriftenreihe302.html} [Accessed on October 16, 2017]},
issn = {21927863} } 
[techreport] bibtexW. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, und A. Rakow, "Traffic Sequence Charts  From Visualization to Semantics,".
@techreport{report/OTR/DKMPR2017,
author = {Werner Damm and Stephanie Kemper and Eike M{\"o}hlmann and Thomas Peikenkamp and Astrid Rakow},
title = {{Traffic Sequence Charts  From Visualization to Semantics}},
institution= {SFB/TR 14 AVACS},
month = {10},
year = {2017},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {117},
} 
[inbook] bibtexW. Damm, E. Möhlmann, T. Peikenkamp, und A. Rakow, "A Formal Semantics for Traffic Sequence Charts.
@INBOOK{,
author = {Damm, Werner and M{\"{o}}hlmann, Eike and Peikenkamp, Thomas and Rakow, Astrid},
month = oct, title = {A Formal Semantics for Traffic Sequence Charts},
year = {2017},
publisher = {Festschrift in honor of Edmund A. Lee} } 
[article] bibtex  Dokument aufrufenE. Althaus, B. Beber, W. Damm, S. Disch, W. Hagemann, A. Rakow, C. Scholl, U. Waldmann, und B. Wirtz, "Verification of linear hybrid systems with large discrete state spaces using counterexampleguided abstraction refinement
@ARTICLE{althaus2017,
author = {Althaus, Ernst and Beber, Bjoern and Damm, Werner and Disch, Stefan and Hagemann, Willem and Rakow, Astrid and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
keywords = {interpolation},
title = {Verification of linear hybrid systems with large discrete state spaces using counterexampleguided abstraction refinement},
journal = {Science of Computer Programming},
volume = {},
number = {},
year = {2017},
pages = {},
issn = {01676423},
url = {http://www.sciencedirect.com/science/article/pii/S0167642317300850},
doi = {https://doi.org/10.1016/j.scico.2017.04.010},
abstract = {We present a counterexampleguided abstraction refinement (CEGAR) approach for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can, in contrast to purely functional controller models, not be analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The presented abstraction methods directly work on a symbolic representation of arbitrary nonconvex combinations of linear constraints and boolean variables using LinAIGs. Several interpolation methods allow us to compute abstractions consisting of fewer linear constraints, and hence reduce the complexity of the reachable state set computation. In combination with methods that guarantee the preciseness of abstractions, this leads to a significant reduction of the runtimes of the verification process compared with exact verification.},
access={restricted},
subproject={H3},
bibtex={althaus.scp2017.bib},
pdf={althaus.scp2017.pdf},
journallong={Science of Computer Programming},
journalshort={SCP},
category={Formal Methods},
crosssite={FB,OL,SB},
}
2016

[techreport] bibtexE. Althaus, B. Beber, W. Damm, S. Disch, W. Hagemann, A. Rakow, C. Scholl, U. Waldmann, und B. Wirtz, "Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization,".
@TECHREPORT{atr103,
author = {Althaus, Ernst and Beber, Björn and Damm, Werner and Disch, Stefan and Hagemann, Willem and Rakow, Astrid and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fränzle, Martin and Olderog, ErnstRüdiger and Podelski, Andreas},
month = {April},
title = {Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {103},
year = {2016},
institution = {SFB/TR 14 AVACS},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = {This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can  in contrast to purely functional controller models  not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.},
access={open},
bibtex={atr103.bib},
pdf={avacs_technical_report_103.pdf},
subproject={H3},
} 
[techreport] bibtexW. Damm, E. Möhlmann, und A. Rakow, "A Design Framework for Concurrent Hybrid Controllers with Safety and Stability Annotations,".
@TECHREPORT{atr105,
author = {Damm, Werner and Möhlmann, Eike and Rakow, Astrid},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fränzle, Martin and Olderog, ErnstRüdiger and Podelski, Andreas},
month = {April},
title = {A Design Framework for Concurrent Hybrid Controllers with Safety and Stability Annotations},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {105},
year = {2016},
institution = {SFB/TR 14 AVACS},
note = {http://www.avacs.org},
abstract = {We present an assume guarantee framework for hybrid sys tems which implements design principles tailored for loosely coupled con trollers of safety critical applications. To bridge the gap between design and implementation level, the framework takes into account signal laten cies and potential loss of coordination messages between controllers on a common plant. Safety as well as stability properties of a controller can be derived compositionally from its subcomponents. Industrial applications usually require safety and stability properties.},
access={open},
bibtex={atr105.bib},
pdf={avacs_technical_report_105.pdf},
subproject={H3,H4},
} 
[techreport] bibtexW. Damm, B. Finkbeiner, und A. Rakow, "Contractbased compositional synthesis of distributed controllers,".
@TECHREPORT{atr115,
author = {Damm, Werner and Finkbeiner, Bernd and Rakow, Astrid},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fränzle, Martin and Olderog, ErnstRüdiger and Podelski, Andreas},
month = {June},
title = {Contractbased compositional synthesis of distributed controllers},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {115},
year = {2016},
institution = {SFB/TR 14 AVACS},
note = {http://www.avacs.org},
abstract = {We present methods build on recent foundational results on compositional synthesis automating three design steps in contractbased system design, and illustrate these for an Advanced Driver Assistance System combining Automatic Cruise Control and Automatic Lane keeping. The design steps we consider are (i) the characterization of library elements, (ii) incremental system design, and (iii) supporting the OEM/supplier interface by synthesizing contracts for subsystems to be developed independently by suppliers.},
access={open},
bibtex={atr115.bib},
pdf={avacs_technical_report_115.pdf},
subproject={S2},
} 
[misc] bibtex  Dokument aufrufenW. Damm, B. Finkbeiner, und A. Rakow, What You Really Need To Know About Your Neighbor.
@MISC{DFR:2016,
author = {Damm, Werner and Finkbeiner, Bernd and Rakow, Astrid},
title = {What You Really Need To Know About Your Neighbor},
year = {2016},
location = {Toronto, Ontario, Canada},
note = {Preproceedings of SYNT2016, 5th Workshop on Synthesis},
url = {http://formal.epfl.ch/synt/2016/papers/paper06.pdf} } 
[inproceedings] bibtexA. Stühring, G. Ehmen, und S. Fröschle, "Analyzing the Impact of Injected Sensor Data on an Advanced Driver Assistance System using the OP2TiMuS Prototyping Platform.
@INPROCEEDINGS{SEFDATE2016,
author = {Stühring, Alexander and Ehmen, Günter and Fröschle, Sibylle},
title = {Analyzing the Impact of Injected Sensor Data on an Advanced Driver Assistance System using the OP2TiMuS Prototyping Platform},
booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe (DATE) 2016},
series = {DATE '16},
year = {2016},
publisher = {European Design and Automation Association},
address = {3001 Leuven, Belgium},
note = {to appear},
abstract = {Modern vehicles are running complex and safety critical applications distributed over several Electronic Control Units (ECUs). Some ECUs are equipped with communication interfaces providing access to other devices, networks or remote services. Since the number of attack vectors is increasing, an early investigation of the impact of attacks becomes steadily more important. This paper gives an example how manipulated sensor data injected to the CAN bus affects an Advanced Driver Assistance System (ADAS). Within multiple experiments we illustrate the impact of different aspects like the sending rate.} }
2015

[article] bibtex  Dokument aufrufenW. Hagemann, "Efficient Geometric Operations on Convex Polyhedra, with an Application to Reachability Analysis of Hybrid Systems, pp. 283325
@ARTICLE{,
author = {Hagemann, Willem},
title = {Efficient Geometric Operations on Convex Polyhedra, with an Application to Reachability Analysis of Hybrid Systems},
journal = {Mathematics in Computer Science},
volume = {9},
number = {3},
year = {2015},
pages = {283325},
url = {http://dx.doi.org/10.1007/s1178601502389},
doi = {10.1007/s1178601502389} } 
[inproceedings] bibtex  Dokument aufrufenE. Moehlmann, W. Hagemann, und O. Theel, "Hybrid Tools for Hybrid Systems  Proving Stability and Safety at Once, pp. 222239.
@INPROCEEDINGS{,
author = {Moehlmann, Eike and Hagemann, Willem and Theel, Oliver},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
title = {Hybrid Tools for Hybrid Systems  Proving Stability and Safety at Once},
booktitle = {Formal Modeling and Analysis of Timed Systems},
series = {Lecture Notes in Computer Science},
volume = {9268},
year = {2015},
pages = {222239},
isbn = {9783319229744},
url = {http://dx.doi.org/10.1007/9783319229751_15},
doi = {10.1007/9783319229751_15} } 
[techreport] bibtexW. Hagemann, E. Moehlmann, und O. Theel, "Hybrid Tools for Hybrid Systems: Proving Stability and Safety at Once  Extended Version,".
@TECHREPORT{atr108,
author = {Hagemann, Willem and Moehlmann, Eike and Theel, Oliver},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fraenzle, Martin and Olderog, ErnstRuediger and Podelski, Andreas},
month = {July},
title = {Hybrid Tools for Hybrid Systems: Proving Stability and Safety at Once  Extended Version},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {108},
year = {2015},
institution = {SFB/TR 14 AVACS},
note = {http://www.avacs.org},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute singlemode Lyapunov functions, unroll the hybrid system's automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the singlemode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the singlemode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
access={open},
bibtex={atr108.bib},
pdf={avacs_technical_report_108.pdf},
subproject={H3,H4},
} 
[techreport] bibtexW. Damm, M. Horbach, und V. SofronieStokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata,".
@TECHREPORT{atr111,
author = {Damm, Werner and Horbach, Matthias and SofronieStokkermans, Viorica},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fraenzle, Martin and Olderog, ErnstRuediger and Podelski, Andreas},
month = {December},
title = {Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {111},
year = {2015},
institution = {SFB/TR 14 AVACS},
note = {http://www.avacs.org},
abstract = {We consider systems composed of an unbounded number of uniformly designed linear hybrid automata, whose dynamic behavior is determined by their relation to neighboring systems. We present a class of such systems and a class of safety properties whose verification can be reduced to the verification of (small) families of ``neighboring'' systems of bounded size, and identify situations in which such verification problems are decidable, resp.\ fixed parameter tractable. We illustrate the approach with an example from coordinated vehicle guidance, and describe an implementation which allows us to perform such verification tasks automatically.},
access={open},
bibtex={atr111.bib},
pdf={avacs_technical_report_111.pdf},
subproject={H3},
} 
[inproceedings] bibtex  Dokument aufrufenW. Hagemann und E. Moehlmann, "Inscribing HPolyhedra in Quadrics using a Projective Generalization of Closed Convex Sets.
@INPROCEEDINGS{conf/cccg/hagemannm2015a,
author = {Hagemann, Willem and Moehlmann, Eike},
title = {Inscribing HPolyhedra in Quadrics using a Projective Generalization of Closed Convex Sets},
booktitle = {Proceedings of the 27th Canadian Conference on Computational Geometry (CCCG 2015), Kingston, Ontario, Canada, 2015},
year = {2015},
url = {http://research.cs.queensu.ca/cccg2015/CCCG.pdf},
abstract = {We present a projective generalization of closed sets, called complete projective embeddings, which allows us to inscribe Hpolyhedra in quadrics efficiently. Essentially, the complete projective embedding of a closed convex set $P \subseteq K^d$ is a double cone in $K^{d+1}$. We show that complete projective embeddings of polyhedral sets are of particular interest and already occurred in the theory of linear fractional programming. Our approach works as follows: By projective principal axis transformation the quadric is converted to a hyperboloid and then approximated by an inner (right) spherical cylinder. Now, given an inscribed Hpolytope of the spherical cross section, cylindrification of the polyhedron yields an inscribed Hpolyhedron of the spherical cylinder and, hence, of the hyperboloid. After application of the inverse base transformation this approach finally yields an inscribed set of the quadric. The crucial task of this procedure is to find an appropriate generalization of closed sets, which is closed under the involved projective transformations and allows us to recover the nonprojective equivalents to the inscribed sets obtained by our approach. It turns out that complete projective embeddings are the requested generalizations.},
access={open},
bibtex={hagemann.cccg2015.bib},
category={other},
conferencelong={Canadian Conference on Computational Geometry},
conferenceshort={CCCG},
crosssite={""},
pdf={hagemann.cccg2015.pdf},
subproject={H3,H4},
} 
[incollection] bibtexW. Damm, M. Horbach, und V. SofronieStokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata, Lutz, C. und Ranise, S., Eds., pp. 186202.
@INCOLLECTION{DammFrocos15,
author = {Damm, Werner and Horbach, Matthias and SofronieStokkermans, Viorica},
editor = {Lutz, Carsten and Ranise, Silvio},
title = {Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata},
booktitle = {Frontiers of Combining Systems},
series = {Lecture Notes in Computer Science},
volume = {9322},
year = {2015},
pages = {186202},
publisher = {Springer International Publishing},
isbn = {9783319242453},
doi = {10.1007/9783319242460_12},
language={English},
} 
[inproceedings] bibtex  Dokument aufrufenW. Damm und A. SangiovanniVincentelli, "A conceptual model of Systems of Systems.
@INPROCEEDINGS{DSV2015,
author = {Damm, Werner and SangiovanniVincentelli, Alberto},
month = {April},
title = {A conceptual model of Systems of Systems},
booktitle = {Proceedings Second International Workshop on the Swarm at the Edge of the Cloud, CPS Week 2015},
year = {2015},
url = {http://terraswarm.org/pubs/556.html},
abstract = {We propose a meta  model for systems of systems which is rich enough to model realistic applications and at the same time can be used as a blue print for identifying typical trouble spots in SoS design(and consequently also for IoT, IoE, networked CPS and swarm systems) as well as guiding the development of distributed strategies for the coordination and orchestration of their constituent system.The talk highlights typical pitfalls in SoS design and explains countermeasures based on the underlying conceptual model.},
day={13},
} 
[incollection] bibtexP. Reinkemeier, A. Benveniste, W. Damm, und I. Stierand, "Contracts for Schedulability Analysis, Sankaranarayanan, S. und Vicario, E., Eds., pp. 270287.
@INCOLLECTION{RBDS+FORMATS2015,
author = {Reinkemeier, Philipp and Benveniste, Albert and Damm, Werner and Stierand, Ingo},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
title = {Contracts for Schedulability Analysis},
booktitle = {Formal Modeling and Analysis of Timed Systems},
series = {Lecture Notes in Computer Science},
volume = {9268},
year = {2015},
pages = {270287},
publisher = {Springer International Publishing},
isbn = {9783319229744},
doi = {10.1007/9783319229751_18},
abstract = {In this paper we propose a framework of Assume / Guarantee contracts for schedulability analysis. Unlike previous work addressing compositional scheduling analysis, our objective is to provide support for the OEM / supplier subcontracting relation. The adaptation of Assume / Guarantee contracts to schedulability analysis requires some care, due to the handling of conflicts caused by shared resources. We illustrate our framework in the context of AUTOSAR methodology now popular in the automotive industry sector.} } 
[article] bibtexE. Boede, H. Daembkes, W. Damm, F. Griebel, F. Koester, K. Lemmer, A. Luedtke, J. Niehaus, und T. Peikenkamp, "SafeTRANS: Safety, Testen und Entwicklungsprozesse hochautomatisierter Systeme, pp. 184200
@ARTICLE{STAF2015,
author = {Boede, Eckard and Daembkes, Heinrich and Damm, Werner and Griebel, Franziska and Koester, Frank and Lemmer, Karsten and Luedtke, Andreas and Niehaus, Juergen and Peikenkamp, Thomas},
title = {SafeTRANS: Safety, Testen und Entwicklungsprozesse hochautomatisierter Systeme},
journal = {Haus der Technik (Expert Verlag)},
volume = {Fahrerassistenz und Aktive Sicherheit},
number = {Volume 137},
year = {2015},
pages = {184200},
abstract = {SafeTRANS ist ein gemeinnuetziger deutscher Verein, der sich insbesondere zum Ziel gesetzt hat, Prozesse, Methoden und Werkzeuge zu erforschen, die die Entwicklung sicherer Embedded Systems in der Verkehrstechnik zu verbessern. Im Januar 2015 wurde dazu ein Arbeitskreis Hochautomatisierte Systeme: Safety, Testen und Entwicklungsprozesse gegruendet. Hierin wollen Teilnehmer aus unterschiedlichen Bereichen der Verkehrstechnik zusammenarbeiten, um gemeinsame Ansaetze fuer die Entwicklung und den Test von hochautomatisierten sicherheitskritischen Systemen zu erarbeiten. Als ein erster gemeinsamer Arbeitspunkt wurde die Definition eines interperabelen Umweltmodels fuer die Umgebung der mobilen Plattform identifiziert. Dieses Ueberblickspaper stellt kurz den Verein SafeTRANS und dessen Arbeitskreis dar und gibt dann einen Ueberblick ueber die Resultate einschlaegiger durch SafeTRANS initiierter Projekte zu Methoden der Modellierung und Absicherung der MenschAssistenzsystemInteraktion und er Sicherheit von Assistenzsystemen.},
ISBN = {9783816933106} }
2014

[inproceedings] bibtexW. Hagemann, E. Möhlmann, und A. Rakow, "Verifying a PI Controller using SoapBox and Stabhyli: Experiences on Establishing Properties for a Steering Controller.
@INPROCEEDINGS{,
author = {Hagemann, Willem and Möhlmann, Eike and Rakow, Astrid},
month = {April},
title = {Verifying a PI Controller using SoapBox and Stabhyli: Experiences on Establishing Properties for a Steering Controller},
series = {ARCH 2014},
year = {2014},
abstract = {In the following we describe practical experiences on verifying a steering controller specification. The hybrid automaton implements a PI control rule and considers the vehicle's velocity as input from the environment. By combining the tools Stabhyli and SoapBox, we establish several safety and liveness properties for the steering controller, including convergence towards an equilibrium.} } 
[incollection] bibtexW. Hagemann, "Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections, Biere, A. und Bloem, R., Eds., pp. 407423.
@INCOLLECTION{,
author = {Hagemann, Willem},
editor = {Biere, Armin and Bloem, Roderick},
title = {Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections},
booktitle = {Computer Aided Verification},
series = {Lecture Notes in Computer Science},
volume = {8559},
year = {2014},
pages = {407423},
publisher = {Springer International Publishing},
isbn = {9783319088662},
doi = {10.1007/9783319088679_27},
language={English},
} 
[inproceedings] bibtex  Dokument aufrufenG. Baumgarten, M. Oertel, A. Rettberg, und M. Götz, "First results of automatic faultinjection in an AUTOSAR toolchain, pp. 170175.
@INPROCEEDINGS{,
author = {Baumgarten, Guilherme and Oertel, Markus and Rettberg, Achim and Götz, Marcelo},
keywords = {Analytical models, AUTOSAR, computer simulation, Embedded system, fault injection, fault port, functional automotive safety, Hardware, ISO 26262, Ports (Computers), Safety, Safety relevant systems, Software, Software architecture, Switches},
month = jul, title = {First results of automatic faultinjection in an AUTOSAR toolchain},
booktitle = {Industrial Informatics (INDIN), 2014 12th IEEE International Conference on},
year = {2014},
pages = {170175},
publisher = {IEEE},
location = {Porto Alegre RS, Brazil},
url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6945503&isnumber=6945470},
doi = {10.1109/INDIN.2014.6945503},
abstract = {Faultinjection is a commonly used method for testing safetyrelevant embedded systems. Especially after the introduction of the ISO 26262 the importance of this technique has gained attention in the automotive domain to test the proper implementation of safety concepts. To enable meaningful tests, the possible random hardware faults need to be aligned in early stages of the development process between the hardware and software developers. Since it is difficult to reason that a system nominal behavior is not affected by the injected faultcode, we aim at an automatic injection of faults into the software units using an AUTOSAR toolchain. An extension in the AUTOSAR design tool is proposed in order to capture fault definitions that shall be used to automatically create triggerable defects in the behavioral models designed with SIMULINK/Targetlink. As first results, it is demonstrated how to integrate faults in Targetlink to be able to use AUTOSAR simulation environments without any further changes to perform faultinjection tests. Furthermore, automatically generated testvectors from requirements are used to trigger the fault injection at runnable level.} } 
[techreport] bibtexW. Damm, W. Hagemann, E. Möhlmann, und A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling,".
@TECHREPORT{atr095,
author = {Damm, Werner and Hagemann, Willem and Möhlmann, Eike and Rakow, Astrid},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fränzle, Martin and Olderog, ErnstRüdiger and Podelski, Andreas},
month = {February},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {95},
year = {2014},
institution = {SFB/TR 14 AVACS},
note = {http://www.avacs.org},
pdf={avacs_technical_report_095.pdf},
subproject={H3,H4},
} 
[inproceedings] bibtexW. Damm, E. Möhlmann, und A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling, pp. 145150.
@INPROCEEDINGS{DBLP:conf/hybrid/DammMR14,
author = {Damm, Werner and Möhlmann, Eike and Rakow, Astrid},
keywords = {AssumeGuarantee, automatic verification, Composition, ComputerAided Design, hybrid systems, interface, Safety, Specifications, stability},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
booktitle = {HSCC},
year = {2014},
pages = {145150},
doi = {10.1145/2562059.2562120},
crossref = {DBLP:conf/hybrid/2014},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.} } 
[incollection] bibtex  Dokument aufrufenS. Fröschle und A. Stühring, "Idea: Security Engineering Principles for Day Two Car2X Applications, pp. 213221.
@INCOLLECTION{ESSOS14,
author = {Fröschle, Sibylle and Stühring, Alexander},
title = {Idea: Security Engineering Principles for Day Two Car2X Applications},
booktitle = {Engineering Secure Software and Systems},
series = {Lecture Notes in Computer Science},
volume = {8364},
year = {2014},
pages = {213221},
publisher = {Springer International Publishing},
url = {http://dx.doi.org/10.1007/9783319048970_14},
doi = {10.1007/9783319048970_14} } 
[inproceedings] bibtexS. Henkler, T. Gezgin, I. Stierand, und A. Rettberg, "Evaluation of a Statebased RealTime Scheduling Analysis Technique.
@INPROCEEDINGS{GHSR14B,
author = {Henkler, Stefan and Gezgin, Tayfun and Stierand, Ingo and Rettberg, Achim},
keywords = {Abstraction Techniques, Model Checking, Realtime systems, Scheduling analysis},
month = jul, title = {Evaluation of a Statebased RealTime Scheduling Analysis Technique},
booktitle = {International Conference on Industrial Informatics (INDIN2014)},
year = {2014},
location = {Porto Alegre},
abstract = {The analysis of realtime properties is crucial in safety critical areas. Systems have to work in a timely manner to offer correct services. The analysis of timing properties is particularly difficult for distributed systems when complex interferences between individual tasks can occur. Considering only critical instances, as analytic approaches do, may deliver pessimistic results leading to higher production costs. In previous works we introduced a statebased approach to validate taskand endtoend deadlines for distributed systems. To improve scalability and reduce the analysis time, the approach computes the state spaces of the individual resources in a compositional fashion. For this, abstraction and composition operations were defined to remove those parts of the inputs of resources which have no influence on the response times of the allocated tasks. In this work, a new abstraction technique is introduced for scenarios where event bursts occur. Further, we extend our approach for systems with cyclic dependencies among the resources. We evaluate our approach on a set of example scenarios and compare the results with the stateoftheart tool Uppaal.} } 
[inproceedings] bibtexT. Gezgin, S. Henkler, I. Stierand, und A. Rettberg, "Impact Analysis for Timing Requirements on RealTime Systems.
@INPROCEEDINGS{GSHR14,
author = {Gezgin, Tayfun and Henkler, Stefan and Stierand, Ingo and Rettberg, Achim},
keywords = {Impact Analysis, Statebased Timing Analysis},
month = aug, title = {Impact Analysis for Timing Requirements on RealTime Systems},
booktitle = {The 20th IEEE International Conference on Embedded and RealTime Computing Systems and Applications (RTCSA 2014)},
year = {2014},
publisher = {IEEE xplore},
location = {Chongqing},
abstract = {The analysis of realtime properties is crucial in safety critical areas, and is particularly difficult for distributed systems as complex interferences between tasks of different priorities can occur. In previous works we have introduced a statebased analysis approach to validate endtoend deadlines for distributed systems, where the state spaces of all resources, such as processors and buses, are computed in a compositional fashion. For this, abstraction and composition operations were defined to adequately handle task and resource dependencies. During the design process of a system changes occur typically on both the specification and implementation level, such that already performed analyses of the system have to be repeated. In this work, we define a methodology to adequately handle such changes and to determine the minimal part of the affected architecture. For this, we define an appropriate refinement relation between state spaces of the resources.We use contracts to further reduce the revalidation effort. This check takes place at a higher design level, where only the specification is considered.} } 
[inproceedings] bibtexI. Stierand, S. Malipatlolla, S. Fröschle, A. Stühring, und S. Henkler, "Integrating the Security Aspect into Design Space Exploration of Embedded Systems.
@INPROCEEDINGS{IS+14,
author = {Stierand, Ingo and Malipatlolla, Sunil and Fröschle, Sibylle and Stühring, Alexander and Henkler, Stefan},
keywords = {design space exploration, Embedded System Design, Formalization, Integration, Security},
month = nov, title = {Integrating the Security Aspect into Design Space Exploration of Embedded Systems},
booktitle = {The 2nd IEEE International Workshop on Reliability and Security Data Analysis (RSDA 2014)},
year = {2014},
abstract = {Conventionally, the process of design space exploration (DSE) in embedded system design considers performance, energy and cost as important objectives for optimization. However, in many domains such as in modern day cars the security aspect is becoming more and more significant. On the other hand, the inclusion of security aspect adds a new dimension to the existing complexity of large design spaces, thus an automated support for this is highly desired. The goal of this work is to integrate the security constraint in an automated DSE process to obtain an architecture which is both costoptimized and secure. In specific, for a given system, our approach defines a formal notion of security, which along with other parameters is fed as an input to the DSE process to obtain an architecture satisfying the defined security and realtime requirements. An evaluation of the proposed approach is also performed using an example automotive embedded system.} } 
[incollection] bibtexW. Damm und B. Finkbeiner, "Automatic Compositional Synthesis of Distributed Systems, Jones, C., Pihlajasaari, P., und Sun, J., Eds., pp. 179193.
@INCOLLECTION{raey,
author = {Damm, Werner and Finkbeiner, Bernd},
editor = {Jones, Cliff and Pihlajasaari, Pekka and Sun, Jun},
title = {Automatic Compositional Synthesis of Distributed Systems},
booktitle = {FM 2014: Formal Methods},
series = {Lecture Notes in Computer Science},
volume = {8442},
year = {2014},
pages = {179193},
publisher = {Springer International Publishing},
isbn = {9783319064093},
doi = {10.1007/9783319064109_13},
language={English},
} 
[inproceedings] bibtexI. Stierand, P. Reinkemeier, und P. Bhaduri, "Virtual Integration of RealTime Systems based on Resource Segregation Abstraction, pp. 115.
@INPROCEEDINGS{StierandReinkemeierBhaduri2014,
author = {Stierand, Ingo and Reinkemeier, Philipp and Bhaduri, Purandar},
month = sep, title = {{Virtual Integration of RealTime Systems based on Resource Segregation Abstraction}},
booktitle = {Proc. Formal Modelling and Analysis of Timed Systems (FORMATS'14)},
year = {2014},
pages = {115},
abstract = {Embedded safetycritical systems must not only be functionally correct but must also provide timely service. It is thus important to have rigorous analysis techniques for determining timing properties of such systems. We consider a layered design process, where timing analysis applies when the system is integrated on a target platform. More precisely, we focus on contractbased design, and ask whether a set of realtime components continues to comply to a given system specification when it is integrated on a common hardware. We present an approach for compositional timing analysis, and define conditions under which the system integration will preserve all the timing properties given by the system specification. Therefore, engineers can negotiate specifications of the individual components a priori, knowing that no integration issues will occur due to shared resource usage. The approach exploits $\omega$languages, which enables analysis techniques based on modelchecking. Such an analysis is shown by a case study.} }
2013

[phdthesis] bibtex  Dokument aufrufenM. Büker, "An Automated SemanticBased Approach for Creating Task Structures,".
@PhdThesis{Bueker2013, Title = {An Automated SemanticBased Approach for Creating Task Structures},
Author = {Büker, Matthias},
School = {Carl von Ossietzky Universität Oldenburg},
Year = {2013},
Abstract = {This work is settled in the area of safetycritical embedded systems and presents a formally funded approach for automatically creating an optimized task structure from a Simulink model. Based on an extended task network formalism, in a first step, a formal translation scheme on Simulink block level is defined. Because the resulting tasks are very finegrained and unbalanced with respect to their required computation demand (denoted as task weight), in a second step, an optimized task structure is created by formally merging tasks with each other. Here, the optimization goal is to minimize intertask communication and to balance the weights of tasks. Additionally, it is formally proven that both the translation and the merging of tasks preserves the formal execution semantics of Simulink. The whole approach was implemented as an automated toolchain and evaluated with the help of a case study.},
Key = {bueker2013},
Keywords = {Embedded systems, Matlab Simulink, optimization, realtime, Task Networks},
Language = {English},
Location = {Oldenburg, Germany},
Owner = {matthias},
Pubstate = {published},
Timestamp = {2014.02.20},
Url = {http://oops.unioldenburg.de/1600/} } 
[misc] bibtex  Dokument aufrufenM. Büker, W. Damm, G. Ehmen, S. Henkler, D. Janssen, I. Stierand, und E. Thaden, From Specification Models to Distributed Embedded Applications: A Holistic UserGuided Approach.
@Misc{BDE+13, Title = {From Specification Models to Distributed Embedded Applications: A Holistic UserGuided Approach},
Author = {Büker, Matthias and Damm, Werner and Ehmen, Günter and Henkler, Stefan and Janssen, Detlef and Stierand, Ingo and Thaden, Eike},
HowPublished = {Published at SAE 2013 World Congress},
Year = {2013},
Abstract = {We introduce a framework that aims at automating significant parts of the design flow in a typical scenario for embedded application development in the automotive domain. Given a specification model of a new automotive feature captured in MatlabSimulink, the framework allocates new functions onto the devices of the hardware architecture such as ECUs and buses considering already deployed functions and the distributed nature of embedded systems used in the automotive industry. The framework is motivated by the iterative design process in industrial practice and subdivided into several steps. In the task creation process a balanced task structure is derived automatically from the specification model. Automatic code generation and execution time analysis for each task demands a semanticspreserving restructuring process of the MatlabSimulink model. The task structure and the generated software tasks serve as input for the automated design space exploration process which has the goal to find a costoptimized extension of the existing target hardware and an allocation of tasks on this modified target hardware. This allocation is sufficient to guarantee both systemlevel timing requirements and deadlines extracted from the MatlabSimulink specification model. Engineers may guide the complete process by running it iteratively and tighten the constraints based on their expert knowledge. This semiautomatic userdriven and transparent optimization process helps to increase acceptance by engineers. For evaluation an industrialmotivated case study of a lanechange driver assistance system and an adaptive cruise control has been used.},
Doi = {10.4271/2013010432},
Owner = {guenter},
Timestamp = {2014.02.20},
Url = {http://papers.sae.org/2013010432/} } 
[article] bibtex  Dokument aufrufenM. Büker, W. Damm, G. Ehmen, S. Henkler, D. Janssen, I. Stierand, und E. Thaden, "From Specification Models to Distributed Embedded Applications: A Holistic UserGuided Approach, pp. 194212
@Article{SAE2013Journal, Title = {From Specification Models to Distributed Embedded Applications: A Holistic UserGuided Approach},
Author = {Büker, Matthias and Damm, Werner and Ehmen, Günter and Henkler, Stefan and Janssen, Detlef and Stierand, Ingo and Thaden, Eike},
Journal = {SAE International Journal of Passenger Cars Electronic and Electrical Systems},
Year = {2013},
Month = may, Note = {Originally published at SAE 2013 World Congress. Selected for Journal publication by the SAE.},
Pages = {194212},
Volume = {6},
Abstract = {We introduce a framework that aims at automating significant parts of the design flow in a typical scenario for embedded application development in the automotive domain. Given a specification model of a new automotive feature captured in MatlabSimulink, the framework allocates new functions onto the devices of the hardware architecture such as ECUs and buses considering already deployed functions and the distributed nature of embedded systems used in the automotive industry. The framework is motivated by the iterative design process in industrial practice and subdivided into several steps. In the task creation process a balanced task structure is derived automatically from the specification model. Automatic code generation and execution time analysis for each task demands a semanticspreserving restructuring process of the MatlabSimulink model. The task structure and the generated software tasks serve as input for the automated design space exploration process which has the goal to find a costoptimized extension of the existing target hardware and an allocation of tasks on this modified target hardware. This allocation is sufficient to guarantee both systemlevel timing requirements and deadlines extracted from the MatlabSimulink specification model. Engineers may guide the complete process by running it iteratively and tighten the constraints based on their expert knowledge. This semiautomatic userdriven and transparent optimization process helps to increase acceptance by engineers. For evaluation an industrialmotivated case study of a lanechange driver assistance system and an adaptive cruise control has been used.},
Doi = {10.4271/2013010432},
ISSN = {19464622},
Owner = {guenter},
Timestamp = {2014.02.20},
Url = {http://saepcelec.saejournals.org/} } 
[article] bibtexW. Damm, H. Peter, J. Rakow, und B. Westphal, "Can we build it: formal synthesis of control strategies for cooperative driver assistance systems, pp. 676725
@Article{DBLP:journals/mscs/DammPRW13, Title = {Can we build it: formal synthesis of control strategies for cooperative driver assistance systems},
Author = {Damm, Werner and Peter, HansJörg and Rakow, Jan and Westphal, Bernd},
Journal = {Mathematical Structures in Computer Science},
Year = {2013},
Number = {4},
Pages = {676725},
Volume = {23},
Bibsource = {DBLP, http://dblp.unitrier.de},
Doi = {10.1017/s0960129512000230},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[incollection] bibtexT. Gezgin, S. Henkler, A. Rettberg, und I. Stierand, "ContractBased Compositional Scheduling Analysis for Evolving Systems, Schirner, G., Götz, M., Rettberg, A., Zanella, M., und Rammig, F., Eds., pp. 272282.
@InCollection{iessGHSR, Title = {ContractBased Compositional Scheduling Analysis for Evolving Systems},
Author = {Gezgin, Tayfun and Henkler, Stefan and Rettberg, Achim and Stierand, Ingo},
Booktitle = {Embedded Systems: Design, Analysis and Verification},
Publisher = {Springer Berlin Heidelberg},
Year = {2013},
Editor = {Schirner, Gunar and Götz, Marcelo and Rettberg, Achim and Zanella, MauroC. and Rammig, FranzJ.},
Pages = {272282},
Series = {IFIP Advances in Information and Communication Technology},
Volume = {403},
Doi = {10.1007/9783642388538_25},
ISBN = {9783642388521},
Keywords = {Abstraction Techniques, Compositional analysis, Model Checking, Realtime systems, Scheduling analysis},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[article] bibtexT. Gezgin, I. Stierand, S. Henkler, und A. Rettberg, "Statebased scheduling analysis for distributed realtime systems, pp. 118
@Article{deamGHSR, Title = {Statebased scheduling analysis for distributed realtime systems},
Author = {Gezgin, Tayfun and Stierand, Ingo and Henkler, Stefan and Rettberg, Achim},
Journal = {Design Automation for Embedded Systems},
Year = {2013},
Pages = {118},
Doi = {10.1007/s1061701391127},
ISSN = {09295585},
Keywords = {Compositional analysis, distributed realtime systems , Scheduling analysis, timed automata, Timing analysis},
Language = {English},
Owner = {guenter},
Publisher = {Springer US},
Timestamp = {2014.02.20} } 
[inproceedings] bibtexS. Malipatlolla und I. Stierand, "Evaluating the Impact of Integrating a Security Module on the RealTime Properties of a System.
@InProceedings{MS+IESS13, Title = {Evaluating the Impact of Integrating a Security Module on the RealTime Properties of a System},
Author = {Malipatlolla, Sunil and Stierand, Ingo},
Booktitle = {International Embedded Systems Symposium (IESS)},
Year = {2013},
Abstract = {With a rise in the deployment of electronics in today's systems especially in automobiles, the task of securing them against various attacks has become a major challenge. In particular, the most vulnerable points are: (i) communication paths between the Electronic Control Units (ECUs) and between sensors & actuators and the ECU, (ii) remote software updates from the manufacturer and the infield system. However, when including additional mechanisms to secure such systems, especially realtime systems, there will be a major impact on the realtime properties and on the overall performance of the system. Therefore, the goal of this work is to deploy a minimal security module in a target realtime system and to analyze its impact on the aforementioned properties of the system, while achieving the goals of secure communication and authentic system update. From this analysis, it has been observed that, with the integration of such a security module into the ECU, the response time of the system is strictly dependent on the utilized communication interface between the ECU processor and the security module. The analysis is performed utilizing the security module operating at different frequencies and communicating over two different interfaces i.e., LowPinCount (LPC) bus and MemoryMapped I/O (MMIO) method.},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[techreport] bibtexP. Reinkemeier, P. Ittershagen, I. Stierand, P. A. Hartmann, S. Henkler, und K. Grüttner, "Seamless Segregation for MultiCore Systems,".
@TechReport{OFFISTR2013+SegMultiCore, Title = {Seamless Segregation for MultiCore Systems},
Author = {Reinkemeier, Philipp and Ittershagen, Philipp and Stierand, Ingo and Hartmann, Philipp A. and Henkler, Stefan and Grüttner, Kim},
Institution = {OFFIS},
Year = {2013},
Month = aug, Type = {Technical Report},
Keywords = {interface, multicore, scheduling , segregation},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[incollection] bibtexP. Reinkemeier und I. Stierand, "Compositional Timing Analysis of RealTime Systems based on Resource Segregation Abstraction, Schirner, G., Götz, M., Rettberg, A., Zanella, M., und Rammig, F., Eds., pp. 181192.
@InCollection{RS+IESS13, Title = {Compositional Timing Analysis of RealTime Systems based on Resource Segregation Abstraction},
Author = {Reinkemeier, Philipp and Stierand, Ingo},
Booktitle = {Embedded Systems: Design, Analysis and Verification},
Publisher = {Springer Berlin Heidelberg},
Year = {2013},
Editor = {Schirner, Gunar and Götz, Marcelo and Rettberg, Achim and Zanella, MauroC. and Rammig, FranzJ.},
Pages = {181192},
Series = {IFIP Advances in Information and Communication Technology},
Volume = {403},
Abstract = {For most embedded safetycritical systems not only the functional correctness is of importance, but they must provide their services also in a timely manner. Therefore, it is important to have rigorous analysis techniques for determining timing properties of such systems. The ever increasing complexity of such realtime systems calls for compositional analysis techniques, where timing properties of local systems are composed to infer timing properties of the overall system. In analytical timing analysis approaches the dynamic timing behavior of a system is characterized by mathematical formulas abstracting from the statedependent behavior of the system. While these approaches scale well and also support compositional reasoning, the results often exhibit large overapproximations. Our approach for compositional timing analysis is based on ωregular languages, which can be employed in automatabased modelchecking frameworks. To tackle the scalability problem due to statespace explosion, we present a technique to abstract an application by means of its resource demands. The technique allows to carry out an analysis independently for each application that shall be deployed on the same platform using its granted resource supply. Integration of the applications on the platform can then be analyzed based on the different resource supplies without considering details of the applications.},
Doi = {10.1007/9783642388538_17},
ISBN = {9783642388521},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[inproceedings] bibtexI. Stierand und S. Malipatlolla, "Exploiting Functional Models to Assess the Security Aspect in Embedded System Design.
@InProceedings{IS+2013, Title = {Exploiting Functional Models to Assess the Security Aspect in Embedded System Design},
Author = {Stierand, Ingo and Malipatlolla, Sunil},
Booktitle = {International Symposium on Security in Computing and Communications (SSCC 2013)},
Year = {2013},
Abstract = {Conventionally, automotive embedded systems are assessed for evaluating various different aspects such as safety, functionality, and realtime. However, the inclusion of security aspect, which indeed is becoming increasingly important in modern day cars, has a significant impact on the above aspects, especially on functionality and realtime. This impact would be clearly visible in the functional model of the embedded system because including security features modifies the data flow in the system. Thus, the goal of this contribution is to assess and evaluate the security aspect in such systems by exploiting their functional models. Such an assessment further results in establishing a possible relation between realtime formal analysis and the existing security theory. For this, a formal approach},
Keywords = {Embedded systems, Formalization, realtime, Security Protocols, Validation.},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[inproceedings] bibtexI. Stierand, P. Reinkemeier, T. Gezgin, und P. Bhaduri, "RealTime Scheduling Interfaces and Contracts for the Design of Distributed Embedded Systems.
@InProceedings{SRG+SIES2013, Title = {RealTime Scheduling Interfaces and Contracts for the Design of Distributed Embedded Systems},
Author = {Stierand, Ingo and Reinkemeier, Philipp and Gezgin, Tayfun and Bhaduri, Purandar},
Booktitle = {Industrial Embedded Systems (SIES), 2013 8th IEEE International Symposium on},
Year = {2013},
Owner = {guenter},
Timestamp = {2014.02.20} } 
[phdthesis] bibtex  Dokument aufrufenE. M. Thaden, "SemiAutomatic Optimization of Hardware Architectures in Embedded Systems,".
@PhdThesis{Thaden2013, Title = {SemiAutomatic Optimization of Hardware Architectures in Embedded Systems},
Author = {Thaden, Eike Martin},
School = {Carl von Ossietzky Universität Oldenburg},
Year = {2013},
Month = may, Note = {Submitted on 20130204.},
Abstract = {The effort for the development of a safetycritical embedded system can be reduced tremendously if a similar existing system is used as basis which is then extended by additional functionality. However, this is a very challenging task because in general for both the already integrated and the new parts of such a system complex constraints have to be satisfied to guarantee their correct functionality. Furthermore, larger embedded systems are typically realized as distributed systems with multiple processors connected by a complex communication infrastructure. This leads to a huge number of design alternatives suitable for the extension of such a system thus complicating the manual search for costefficient solutions or even rendering it impossible. Searching entirely automatically is not too promising as well because usually lots of informal requirements have to be satisfied, some of which are concretized while already searching for possible solutions. In this work a semiautomatic approach for the optimization of hardware architectures of embedded systems is presented that supports developers in extending existing systems by adding additional functionality implemented as software tasks. The twotier optimization process explores the design space defined by constraints for valid allocations of the software tasks to the hardware architecture. If necessary, existing processors can be replaced by more powerful ones or additional processors can be integrated while aiming for a costefficient hardware architecture. The optimization approach exploits that larger embedded systems typically use a hierarchical structure where the hardware architecture is composed from hardware subsystems: Firstly, a global (systemwide) optimization step computes preallocations of all additional software tasks onto subsystems based on an abstract characterization of the required and provided computation capacity. Separately for each subsystem, the preallocated tasks are then allocated to processors by local optimization steps under consideration of all subsystemspecific constraints. Software tasks that could not be allocated are handed back to the global tier for being allocated in later iterations. Exact optimization methods are presented for both the global and the local optimization steps. Finally, the results of an extensive evaluation based on three benchmarks are presented. In this evaluation both optimization methods have been compared with alternative approaches.},
Key = {thaden2013},
Keywords = {design space exploration, Embedded systems, optimization, realtime, scheduling },
Location = {Oldenburg, Lower Saxony, Germany},
Owner = {guenter},
Timestamp = {2014.02.20},
Url = {http://oops.unioldenburg.de/id/eprint/1491} }
2012

[techreport] bibtex  Dokument aufrufenA. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J. Raclet, P. Reinkemeier, A. SangiovanniVincentelli, W. Damm, T. Henzinger, und K. G. Larsen, "Contracts for System Design,".
@TECHREPORT{benveniste:hal00757488,
author = {Benveniste, Albert and Caillaud, Benoit and Nickovic, Dejan and Passerone, Roberto and Raclet, JeanBaptiste and Reinkemeier, Philipp and SangiovanniVincentelli, Alberto and Damm, Werner and Henzinger, Thomas and Larsen, Kim G.},
title = {Contracts for System Design},
institution = {INRIA},
year = {2012},
type = {Rapport de recherche},
number = {RR8147},
month = nov, abstract = {{Systems design has become a key challenge and differentiating factor over the last decades for system companies. Aircrafts, trains, cars, plants, distributed telecommunication military or health care systems, and more, involve systems design as a critical step. Complexity has caused system design times and costs to go severely over budget so as to threaten the health of entire industrial sectors. Heuristic methods and standard practices do not seem to scale with complexity so that novel design methods and tools based on a strong theoretical foundation are sorely needed. Modelbased design as well as other methodologies such as layered and compositional design have been used recently but a unified intellectual framework with a complete design flow supported by formal tools is still lacking albeit some attempts at this framework such as Platformbased Design have been successfully deployed. Recently an "orthogonal" approach has been proposed that can be applied to all methodologies proposed thus far to provide a rigorous scaffolding for verification, analysis and abstraction/refinement: contractbased design. Several results have been obtained in this domain but a unified treatment of the topic that can help in putting contractbased design in perspective is still missing. This paper intends to provide such treatment where contracts are precisely defined and characterized so that they can be used in design methodologies such as the ones mentioned above with no ambiguity. In addition, the paper provides an important link between interfaces and contracts to show similarities and correspondences. Examples of the use of contracts in design are provided as well as in depth analysis of existing literature.}},
affiliation = {S4  INRIA  IRISA , AIT Austrian Institute of Technology , Department of Information Engineering and Computer Science  DISI , Institut de recherche en informatique de Toulouse  IRIT , OFFIS [Oldenburg] , Electrical Engineering and Computer Science [Berkeley]  EECS , Institute of Science and Technology [Austria]  IST Austria , University of Aalborg},
hal_id = {hal00757488},
keywords = {component based design, contract, interface, system design},
language = {Anglais},
owner = {guenter},
pages = {65},
timestamp = {2013.06.03},
url = {http://hal.inria.fr/hal00757488 \nhttp://hal.inria.fr/hal00757488/PDF/RR8147.pdf} } 
[incollection] bibtex  Dokument aufrufenM. Broy, W. Damm, S. Henkler, K. Pohl, A. Vogelsang, und T. Weyer, "Introduction to the SPES Modeling Framework, pp. 3149.
@INCOLLECTION{Broy.Damm.etal2012,
author = {Broy, Manfred and Damm, Werner and Henkler, Stefan and Pohl, Klaus and Vogelsang, Andreas and Weyer, Thorsten},
title = {Introduction to the SPES Modeling Framework},
booktitle = {ModelBased Engineering of Embedded Systems},
publisher = {Springer},
year = {2012},
chapter = {3},
pages = {3149},
address = {Berlin Heidelberg},
abstract = {Today’s and, even more so, the future development of embedded systems faces a variety of challenges. Key success factors to meeting these challenges are suitable concepts for abstraction and structure at different levels of granularity. The result of these concepts is a seamless development approach that heavily facilitates reuse and automation. A basic requirement for such a seamless approach is a clear notion of a system that is formalized by a comprehensive modeling theory. According to this modeling theory, a modeling framework has to provide appropriate models and description techniques for modeling the different aspects and artifacts of system development. This section explains these conclusions and introduces the idea of system and the modeling framework. It also references the modeling theories used in SPES.},
doi = {10.1007/9783642346149_3},
isbn = {9783642346132},
owner = {guenter},
timestamp = {2013.06.03},
url = {http://link.springer.com/chapter/10.1007/9783642346149_3} } 
[inbook] bibtex  Dokument aufrufenM. Büker, K. Grüttner, P. A. Hartmann, und I. Stierand, "Mapping of Concurrent ObjectOriented Models to Extended RealTime Task Networks, pp. 3754.
@INBOOK{BuekerGruettnerHartmannStierand2012, pages = {3754},
title = {Mapping of Concurrent ObjectOriented Models to Extended RealTime Task Networks},
publisher = {Springer},
year = {2012},
author = {Büker, Matthias and Grüttner, Kim and Hartmann, Philipp A. and Stierand, Ingo},
month = {01},
booktitle = {System Specification and Design Languages  Selected Contributions from FDL 2010},
isbn = {9781461414261},
owner = {guenter},
timestamp = {2013.06.03},
url = {http://www.springer.com/9781461414261} } 
[inproceedings] bibtexT. Gezgin, S. Henkler, A. Rettberg, und I. Stierand, "Abstraction Techniques for Compositional Statebased Scheduling Analysis.
@INPROCEEDINGS{GezginHenklerRettbergStierand2012,
author = {Gezgin, Tayfun and Henkler, Stefan and Rettberg, Achim and Stierand, Ingo},
title = {Abstraction Techniques for Compositional Statebased Scheduling Analysis},
booktitle = {Brazilian Symposium on Computing System Engineering (SBESC)},
year = {2012},
month = {November},
owner = {guenter},
timestamp = {2013.06.03} } 
[phdthesis] bibtex  Dokument aufrufenH. Jost, "Reasoning on Domain Knowledge and Technical Standards to Support the Development of SafetyCritical Automotive Systems,".
@PHDTHESIS{Jost:PhDThesis12,
author = {Jost, Henning},
title = {Reasoning on Domain Knowledge and Technical Standards to Support the Development of SafetyCritical Automotive Systems},
school = {Carl von Ossietzky Universität Oldenburg, Germany},
year = {2012},
note = {ISBN: 9783843905701},
keywords = {uniol2012sesdamm},
owner = {guenter},
timestamp = {2013.06.03},
url = {http://www.dr.hutverlag.de/9783843905701.html} } 
[incollection] bibtexA. Rakow, "Safety Slicing Petri Nets, Haddad, S. und Pomello, L., Eds., pp. 268287.
@INCOLLECTION{rakow12,
author = {Rakow, Astrid},
title = {Safety Slicing Petri Nets},
booktitle = {Application and Theory of Petri Nets},
publisher = {Springer Berlin Heidelberg},
year = {2012},
editor = {Haddad, Serge and Pomello, Lucia},
volume = {7347},
series = {Lecture Notes in Computer Science},
pages = {268287},
doi = {10.1007/9783642311314_15},
isbn = {9783642311307},
owner = {guenter},
timestamp = {2013.06.03} } 
[article] bibtex  Dokument aufrufenA. L. SangiovanniVincentelli, W. Damm, und R. Passerone, "Taming Dr. Frankenstein: ContractBased Design for CyberPhysical Systems., pp. 217238
@ARTICLE{VincentelliDP12,
author = {SangiovanniVincentelli, Alberto L. and Damm, Werner and Passerone, Roberto},
title = {Taming Dr. Frankenstein: ContractBased Design for CyberPhysical Systems.},
journal = {Eur. J. Control},
year = {2012},
volume = {18},
pages = {217238},
number = {3},
addedat = {20121106T00:00:00.000+0100},
biburl = {http://www.bibsonomy.org/bibtex/2b5bb1119a3761b3ded70b53cab31ac7c/dblp},
doi = {10.3166/ejc.18.217238},
interhash = {bfdf1df55f32dd0a940d801cd946af14},
intrahash = {b5bb1119a3761b3ded70b53cab31ac7c},
keywords = {dblp},
owner = {guenter},
timestamp = {20121106T00:00:00.000+0100},
url = {http://dblp.unitrier.de/db/journals/ejcon/ejcon18.html#SangiovanniVincentelliDP12} } 
[inproceedings] bibtexT. Toben und J. Rakow, "Safety and Precision of Spatial Context Models for Autonomous Systems.
@INPROCEEDINGS{toben12,
author = {Toben, Tobe and Rakow, JanHendrik},
title = {Safety and Precision of Spatial Context Models for Autonomous Systems},
booktitle = {Proceedings of the 1st ETAPS Workshop on "Hybrid Autonomous Systems" (HAS 2011)},
year = {2012},
publisher = {ENTCS},
location = {Saarbrücken, Germany},
owner = {guenter},
timestamp = {2013.06.03} }
2011

[techreport] bibtexM. Büker, W. Damm, G. Ehmen, A. Metzner, I. Stierand, und E. Thaden, "Automating the design flow for distributed embedded automotive applications: keeping your time promises, and optimizing costs, too,".
@TECHREPORT{atr069,
author = {B\"{u}ker, Matthias and Damm, Werner and Ehmen, G\"{u}nter and Metzner, Alexander and Stierand, Ingo and Thaden, Eike},
title = {Automating the design flow for distributed embedded automotive applications: keeping your time promises, and optimizing costs, too},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {69},
note = {ISSN: 18609821, http://www.avacs.org.},
abstract = {We address the complete design flow from specification models of new automotive functions captured in MatlabSimulink to their distributed execution on hierarchical busbased electronic architectures hosting the release of already deployed automotive functions. We propose an automated design space exploration process resulting in a costoptimized extension of the existing target hardware and an allocation of balanced task structures automatically derived from the specification model on this modified target hardware which is sufficient to guarantee both systemlevel timing requirements and deadlines extracted from the MatlabSimulink specification model.},
access = {open},
bibtex = {atr069.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_069.pdf},
series = {ATR},
subproject = {R2} } 
[inproceedings] bibtexM. Büker, W. Damm, G. Ehmen, A. Metzner, I. Stierand, und E. Thaden, "Automating the Design Flow for Distributed Embedded Automotive Applications: Keeping Your Time Promises, and Optimizing Costs, too.
@INPROCEEDINGS{buekeretal2011,
author = {B\"{u}ker, Matthias and Damm, Werner and Ehmen, G\"{u}nter and Metzner, Alexander and Stierand, Ingo and Thaden, Eike},
title = {Automating the Design Flow for Distributed Embedded Automotive Applications: Keeping Your Time Promises, and Optimizing Costs, too},
booktitle = {Proc. International Symposium on Industrial Embedded Systems (SIES'11)},
year = {2011},
abstract = {We address the complete design flow from specification models of new automotive functions captured in MatlabSimulink to their distributed execution on hierarchical busbased electronic architectures hosting the release of already deployed automotive functions. We propose an automated design space exploration process resulting in a costoptimized extension of the existing target hardware and an allocation of balanced task structures automatically derived from the specification model on this modified target hardware which is sufficient to guarantee both systemlevel timing requirements and deadlines extracted from the MatlabSimulink specification model.},
access = {restricted},
bibtex = {bueker.sies11.bib},
keywords = {uniol2011sesdamm},
pdf = {bueker.sies11.pdf},
subproject = {R2} } 
[inproceedings] bibtexM. Büker, W. Damm, G. Ehmen, und I. Stierand, "An Automated SemanticBased Approach for Creating Tasks from Matlab Simulink Models.
@INPROCEEDINGS{Buker2011a,
author = {B\"{u}ker, Matthias and Damm, Werner and Ehmen, G\"{u}nter and Stierand, Ingo},
title = {{An Automated SemanticBased Approach for Creating Tasks from Matlab Simulink Models}},
booktitle = {Proc. of 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)},
year = {2011},
keywords = {uniol2011sesdamm},
owner = {guenter},
timestamp = {2011.05.10} } 
[techreport] bibtex  Dokument aufrufenA. Baumgart, E. Böde, M. Büker, W. Damm, G. Ehmen, T. Gezgin, S. Henkler, H. Hungar, B. Josko, M. Oertel, T. Peikenkamp, P. Reinkemeier, I. Stierand, und R. Weber, "Architecture Modeling,".
@TECHREPORT{OFFISTR2011+AM,
author = {Baumgart, Andreas and Böde, Eckard and Büker, Matthias and Damm, Werner and Ehmen, Günter and Gezgin, Tayfun and Henkler, Stefan and Hungar, Hardi and Josko, Bernhard and Oertel, Markus and Peikenkamp, Thomas and Reinkemeier, Philipp and Stierand, Ingo and Weber, Raphael},
title = {Architecture Modeling},
institution = {OFFIS},
year = {2011},
type = {Technical Report},
month = mar, keywords = {architecture, component based design, contract based design, MetaModel},
owner = {guenter},
timestamp = {2013.08.05},
url = {http://ses.informatik.unioldenburg.de/download/bib/paper/OFFISTR2011_ArchitectureModeling.pdf} } 
[techreport] bibtexM. Büker, T. Gezgin, und I. Stierand, "On the Implementability of Complex RealTime Systems,".
@TECHREPORT{MBTGIS:Boundedness,
author = {Matthias B{\"u}ker and Tayfun Gezgin and Ingo Stierand},
title = {On the Implementability of Complex RealTime Systems},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {68},
note = {ISSN: 18609821, http://www.avacs.org.},
abstract = {Realtime scheduling theory is a powerful technique for efficient analysis of system behaviour. Task Networks as common formalisms for scheduling analysis however often lack expressive power to model functional behaviour like for example different modes of operation. Research focuses on combining different formalisms to raise the expressiveness while maintaining efficient realtime analysis methods. There are rare approaches to extend task network formalisms itself. Though, this would allow a tight integration of scheduling analysis and other verification techniques. Realtime scheduling analysis however heavily relies on decidability of boundedness for executions, and this is not necessarily ensured for more complex formalisms. We discuss such an extended formalism able to model complex realtime systems, and we show that boundedness is still decidable here.},
access = {open},
bibtex = {atr068.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_068.pdf},
series = {ATR},
subproject = {R2} } 
[inproceedings] bibtexB. Clark, I. Stierand, und E. Thaden, "CostMinimal PreAllocation of Software Tasks Under RealTime Constraints.
@INPROCEEDINGS{ClarkStierandThaden2011,
author = {Clark, Brian and Stierand, Ingo and Thaden, Eike},
title = {CostMinimal PreAllocation of Software Tasks Under RealTime Constraints},
booktitle = {Research in Applied Computation Symposium (RACS 2011)},
year = {2011},
abstract = {In this paper we motivate, mathematically formulate, and evaluate a novel approach for finding good preallocations for software tasks together with their communication messages onto a hardware system. The hardware system is composed of subsystems connected via a global communication bus. Each subsystem contains one or more processors whose type can be chosen from a set of processor types with different properties, such as monetary cost, available memory, etc. The overall optimization objective is to minimize the sum of all processor costs. This is done using a Satisfiability Modulo Theories solver with an extension for performing binary search on input variables.},
keywords = {design space exploration, Embedded systems, realtime analysis, uniol2011sesdamm},
owner = {guenter},
timestamp = {2012.01.30} } 
[article] bibtexW. Damm, H. Dierks, S. Disch, W. Hagemann, F. Pigorsch, C. Scholl, U. Waldmann, und B. Wirtz, "Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces
@ARTICLE{DDD+:2011,
author = {Werner Damm and Henning Dierks and Stefan Disch and Willem Hagemann and Florian Pigorsch and Christoph Scholl and Uwe Waldmann and Boris Wirtz},
title = {Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces},
journal = {Science of Computer Programming, Special Issue on Automated Verification of Critical Systems},
year = {2011},
note = {Accepted for publication},
abstract = {We propose an improved symbolic algorithm for the verification of linear hybrid automata with large discrete state spaces (where an explicit representation of discrete states is difficult). Here both the discrete part and the continuous part of the hybrid state space are represented by one symbolic representation called LinAIGs. LinAIGs represent (possibly nonconvex) polyhedra extended by boolean variables. Key components of our method for state space traversal are redundancy elimination and constraint minimization: Redundancy elimination eliminates socalled redundant linear constraints from LinAIG representations by a suitable exploitation of the capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra by exploiting the fact that states already reached in previous steps can be interpreted as 'don't cares' in the current step. Experimental results (including comparisons to the stateoftheart model checkers PHAVer and RED) demonstrate the advantages of our approach.},
access = {restricted},
bibtex = {damm.scp11.bib},
keywords = {uniol2011sesdamm},
pdf = {damm.scp11.pdf},
publisher = {Elsevier},
subproject = {H3} } 
[techreport] bibtexW. Damm, S. Disch, W. Hagemann, C. Scholl, U. Waldmann, und B. Wirtz, "Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems,".
@TECHREPORT{atr76,
author = {Werner Damm and Stefan Disch and Willem Hagemann and Christoph Scholl and Uwe Waldmann and Boris Wirtz},
title = {Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {76},
month = {July},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = {We describe an approach to integrate incremental flow pipe computation into a fully symbolic backward model checker for hybrid systems. Our method combines the advantages of symbolic state set representation, such as the ability to deal with large numbers of boolean variables, with an efficient way to handle continuous flows defined by linear differential equations, possibly including bounded disturbances.},
access = {open},
bibtex = {atr076.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_076.pdf},
series = {ATR},
subproject = {H3} } 
[inproceedings] bibtexW. Damm und B. Finkbeiner, "Does It Pay to Extend the Perimeter of a World Model.
@INPROCEEDINGS{dammfinkbeinerfm2011,
author = {Werner Damm and Bernd Finkbeiner},
title = {Does It Pay to Extend the Perimeter of a World Model?},
booktitle = {Proceedings of the 17th International Symposium on Formal Methods},
year = {2011},
editor = {Michael Butler and Wolfram Schulte},
series = {Lecture Notes in Computer Science},
month = {June},
note = {to appear},
abstract = {Will the cost for observing additional realworld phenomena in a world model be recovered by the resulting increase in the quality of the implementations based on the model? We address the quest for optimal models in light of industrial practices in systems engineering, where the development of control strategies is based on combined models of a system and its environment. We introduce the notion of remorsefree dominance between strategies, where one strategy is preferred over another if it outperforms the other strategy in comparable situations, even if neither strategy is guaranteed to achieve all objectives. We call a world model optimal if it is sufficiently precise to allow for a remorsefree dominating strategy that is guaranteed to remain dominant even if the world model is refined. We present algorithms for the automatic verification and synthesis of dominant strategies, based on tree automata constructions from reactive synthesis.},
access = {restricted},
bibtex = {damm.FM2011.bib},
keywords = {uniol2011sesdamm},
pdf = {damm.FM2011.pdf},
subproject = {S2} } 
[techreport] bibtexW. Damm, C. Ihlemann, und V. SofronieStokkermans, "PTIME parametric verification of safety properties for reasonable linear hybrid automata,".
@TECHREPORT{atr070,
author = {Werner Damm and Carsten Ihlemann and Viorica SofronieStokkermans},
title = {{PTIME} parametric verification of safety properties for reasonable linear hybrid automata},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {70},
note = {ISSN: 18609821, http://www.avacs.org.},
abstract = {This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and timebounded reachability can be decided in nondeterministic polynomial time for nonparametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some modeinvariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.},
access = {open},
bibtex = {atr070.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_070.pdf},
series = {ATR},
subproject = {H3} } 
[inproceedings] bibtexW. Damm, C. Ihlemann, und V. SofronieStokkermans, "Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata.
@INPROCEEDINGS{dammihlemannsofroniehscc11,
author = {Damm, Werner and Ihlemann, Carsten and SofronieStokkermans, Viorica},
title = {Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata},
booktitle = {Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, April 1214, 2011},
year = {2011},
editor = {Frazzoli, Emilio and Grosu, Radu},
publisher = {ACM},
note = {To appear},
abstract = {This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of safety properties with exhaustive entry conditions can be verified in polynomial time and timebounded reachability with exhaustive entry conditions can be decided in nondeterministic polynomial time for nonparametric verification and in exponential time for parametric verification. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.},
access = {restricted},
bibtex = {damm.hscc11.bib},
keywords = {uniol2011sesdamm},
pdf = {damm.hscc11.pdf},
subproject = {H3} } 
[article] bibtexW. Damm, C. Ihlemann, und V. SofronieStokkermans, "PTIME parametric verification of safety properties for reasonable linear hybrid automata
@ARTICLE{dammetallmics11,
author = {Werner Damm and Carsten Ihlemann and Viorica SofronieStokkermans},
title = {{PTIME} parametric verification of safety properties for reasonable linear hybrid automata},
journal = {Mathematics in Computer Science, Special Issue on Numerical Software Verification},
year = {2011},
note = {Accepted for publication},
abstract = {This paper identifies an industrially relevant class of linear hybrid automata (LHA) called 'reasonable LHA' for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and timebounded reachability can be decided in nondeterministic polynomial time for nonparametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some modeinvariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time. },
access = {restricted},
bibtex = {damm.mics11.bib},
editor = {Stefan Ratschan and Georgios Fainekos and Eric Goubault and Sylvie Putot},
keywords = {uniol2011sesdamm},
pdf = {damm.mics11.pdf},
subproject = {H3} } 
[article] bibtexW. Damm, H. Peter, J. Rakow, und B. Westphal, "Can we build it: Formal Synthesis of control strategies for cooperative driver assistance systems
@ARTICLE{damm+rakow+westphalmscs,
author = {Werner Damm and HansJ{\"{o}}rg Peter and Jan Rakow and Bernd Westphal},
title = {Can we build it: Formal Synthesis of control strategies for cooperative driver assistance systems},
journal = {Mathematical Structures in Computer Science, Special Issue on Practical and Lightweight Formal Methods for the Design, Modeling and Analysis of Software Systems},
year = {2011},
note = {Accepted for publication},
abstract = { We propose a design and verificationmethodology supporting the early phases of system design for cooperative driver assistance systems, focussing on realizability of new automotive functions. Specifically, we focus on applications where drivers are supported in complex driving tasks by safe strategies involving coordinated movements of multiple vehicles to successfully complete the driving task. We propose a divide and conquer approach for formally verifying timed probabilistic requirements on successful completion of the driving task and collision freedom, based on formal specifications of a set of given manoeuvring and communication capabilities of the car, allowing in particular to assess, whether these are sufficient to implement strategies for successful completion of the driving task. },
access = {restricted},
bibtex = {damm.mscs11.bib},
editor = {Assaf Kfoury and Azer Bestavros},
keywords = {uniol2011sesdamm},
pdf = {damm.mscs11.pdf},
subproject = {S2} } 
[techreport] bibtexW. Damm, J. Rakow, und B. Westphal, "Can we build it: Formal Synthesis of control strategies for cooperative driver assistance systems,".
@TECHREPORT{atr073,
author = {Werner Damm and Jan Rakow and Bernd Westphal},
title = {Can we build it: Formal Synthesis of control strategies for cooperative driver assistance systems},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {73},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = { We propose a design and verificationmethodology supporting the early phases of system design for cooperative driver assistance systems, focussing on realizability of new automotive functions. Specifically, we focus on applications where drivers are supported in complex driving tasks by safe strategies involving coordinated movements of multiple vehicles to successfully complete the driving task. We propose a divide and conquer approach for formally verifying timed probabilistic requirements on successful completion of the driving task and collision freedom, based on formal specifications of a set of given manoeuvring and communication capabilities of the car, allowing in particular to assess, whether these are sufficient to implement strategies for successful completion of the driving task. },
access = {open},
bibtex = {atr073.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_073.pdf},
series = {ATR},
subproject = {S2} } 
[techreport] bibtexR. Ehlers, M. E. Hahn, M. Mehlmann, H. Peter, J. Rakow, T. Toben, und B. Westphal, "Dynamic Communicating Probabilistic Timed Automata Playing Games,".
@TECHREPORT{atr75,
author = {R{\"u}diger Ehlers and E. Moritz Hahn and Martin Mehlmann and HansJ{\"o}rg Peter and Jan Rakow and Tobe Toben and Bernd Westphal},
title = {Dynamic Communicating Probabilistic Timed Automata Playing Games},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {75},
month = {July},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = { Systems of Systems (SoS) comprising a varying number of communicating processes (or agents) are getting ever more important. As of yet, formal modeling languages and specification logics address isolated features of SoS only. We propose the concise modeling language DCS++ and the property specification logic DPTATL that address all relevant SoS aspects in a unified gametheoretic framework. Language and logic turn out to be an orthogonal extension of wellknown modeling formalisms and logics. Both modeling and specification languages are demonstrated on a nontrivial network routing example.},
access = {open},
bibtex = {atr075.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_075.pdf},
series = {ATR},
subproject = {S2} } 
[inproceedings] bibtexH. Jost, S. Köhler, und F. Köster, "Towards a Safer Development of Driver Assistance Systems by Applying RequirementsBased Methods.
@INPROCEEDINGS{Jost:ITSC2011,
author = {Henning Jost and Silke {K{\"{o}}hler} and Frank {K{\"{o}}ster}},
title = {{T}owards a {S}afer {D}evelopment of {D}river {A}ssistance {S}ystems by {A}pplying {R}equirements{B}ased {M}ethods},
booktitle = {{P}roceedings of the 14th {I}nternational {IEEE} {C}onference on {I}ntelligent {T}ransportation {S}ystems  {ITSC} 2011},
year = {2011},
month = {October},
keywords = {uniol2011sesdamm} } 
[inproceedings] bibtexJ. D. Quesel, M. Fränzle, und W. Damm, "Crossing the bridge between similar games.
@INPROCEEDINGS{avacsh3brg11,
author = {J.D. Quesel AND M. Fr\"{a}nzle AND W. Damm},
title = {Crossing the bridge between similar games},
booktitle = {Formal Modeling and Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg, Denmark, 2123 September, 2011. Proceedings},
year = {2011},
editor = {Stavros Tripakis and Uli Fahrenberg},
series = {Lecture Notes in Computer Science (LNCS)},
month = {Sep.},
publisher = {SpringerVerlag},
note = {15 pp. Accepted for publication on 8 July 2011.},
abstract = { Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. In this paper, we identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.},
access = {restricted},
bibtex = {quesel.formats11.bib},
keywords = {uniol2011sesdamm, uniol2011hsfränzle},
pdf = {quesel.formats11.pdf},
subproject = {H1/2,H3} } 
[inproceedings] bibtexP. Reinkemeier, I. Stierand, P. Rehkop, und S. Henkler, "A patternbased requirement specification language: Mapping automotive specific timing requirements.
@INPROCEEDINGS{RSLvsTADL2011,
author = {Philipp Reinkemeier and Ingo Stierand and Philip Rehkop and Stefan Henkler},
title = {A patternbased requirement specification language: Mapping automotive specific timing requirements},
booktitle = {Software Engineering 2011  Workshopband},
year = {2011},
series = {LNI},
publisher = {GI},
keywords = {uniol2011sesdamm},
owner = {guenter},
timestamp = {2011.05.13} } 
[inproceedings] bibtexA. SangiovanniVincentelli, W. Damm, und R. Passerone, "Taming Dr. Frankenstein: ContractBased Design for CyberPhysical Systems.
@INPROCEEDINGS{SangiovanniVincentelli2011,
author = {Alberto SangiovanniVincentelli and Werner Damm and Roberto Passerone},
title = {Taming Dr. Frankenstein: ContractBased Design for CyberPhysical Systems},
booktitle = {50th IEEE Conference on Decision and Control},
year = {2011},
month = {December},
organization = {IEEE},
keywords = {uniol2011sesdamm},
owner = {guenter},
timestamp = {2012.02.01} } 
[techreport] bibtexB. Westphal, I. Stierand, und T. Gezgin, "Observerbased ModelChecking of RealTime Live Sequence Charts for Uppaal,".
@TECHREPORT{atr071,
author = {Bernd Westphal and Ingo Stierand and Tayfun Gezgin},
title = {Observerbased ModelChecking of RealTime Live Sequence Charts for Uppaal},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {71},
note = {ISSN: 18609821, http://www.avacs.org.},
abstract = {Formalisation and verification of requirements is an inevitable task in safetycritical system design. Requirements on networks of timed automata comprise statements about the existence, timeliness, and order of interautomaton communication, possibly also referring to values of variables and clocks. A natural formalism to capture such requirements is the Live Sequence Charts (LSC) language, which in particular has means to refer to dense time. In this work, we provide an observer based modelchecking procedure for the practically relevant fragment of the LSC language in terms of timed automaton semantics of the verification tool Uppaal. Our approach uses the standard LSC semantics defined in terms of the socalled unwinding structure. We show that LSC verification reduces to deadlock or leadsto verification as supported by Uppaal, thereby obtain observer based LSC verification for safety and liveness properties. },
access = {open},
bibtex = {atr071.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_071.pdf},
series = {ATR},
subproject = {R2} } 
[techreport] bibtexB. Westphal, I. Stierand, T. Gezgin, und H. Dierks, "The Power of Uppaal  A languagebased characterisation of verification complexity,".
@TECHREPORT{atr072,
author = {Bernd Westphal and Ingo Stierand and Tayfun Gezgin and Henning Dierks },
title = {The Power of Uppaal  A languagebased characterisation of verification complexity},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {72},
note = {ISSN: 18609821, http://www.avacs.org.},
abstract = { Observer based verification is an appropriate technique for checking complex requirements for systems defined in terms of automata. Since Uppaal is known as an efficient tool for model checking of timed automata based systems, it has received much attention. Recently, the class of properties verifiable with Uppaal's reachability checking capabilities has been characterized by a specification logic. In this article we provide a timed languagebased characterization of the same class. Moreover, we show that there is a proper superset of additional (liveness) properties that can be checked by using the features of Uppaal. We characterize also these properties as a class of timed languages. },
access = {open},
bibtex = {atr072.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_072.pdf},
series = {ATR},
subproject = {R2} } 
[techreport] bibtexB. Wirtz, T. Strazny, J. Rakow, und A. Rakow, "A Lane Change Assistence Systen: Cooperation and Hybrid Control,".
@TECHREPORT{atr078,
author = {Boris Wirtz and Tim Strazny and Jan Rakow and Astrid Rakow},
title = {A Lane Change Assistence Systen: Cooperation and Hybrid Control},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {78},
month = {July},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = { Automated Highway Systems (AHS's) are considered as a key technology that promises increased safety, reduced energy consumption and optimized traffic flow. Safe and dependable operation of AHS's is of paramount importance and requires the application of rigid formal methods at design time. In this report we present a model for a lane change assistance system which is meant to serve as a foundation for benchmarks boosting theoretic and algorithmic advances in formal verification of the challenging class of cyberphysical systems. The assistance system implements an autonomous lane change manoeuvre conducted in cooperation with other communicating agents. The model implements a layered design for traffic agents where aspects of communication and autonomous control are described as realtime and hybrid systems, respectively, which are intertwined by synchronous message passing. },
access = {open},
bibtex = {atr078.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
keywords = {uniol2011sesdamm},
pdf = {avacs_technical_report_078.pdf},
series = {ATR},
subproject = {H3} }
2010

[inproceedings] bibtexM. Büker, K. Grüttner, P. A. Hartmann, und I. Stierand, "Mapping of Concurrent ObjectOriented Models to Extended RealTime Task Networks.
@InProceedings{ buker2010,
author = {Büker, Matthias and Grüttner, Kim and Hartmann, Philipp A. and Stierand, Ingo},
title = {{Mapping of Concurrent ObjectOriented Models to Extended RealTime Task Networks}},
booktitle = {Proc. Forum on specification \& Design Languages (FDL)},
year = {2010},
abstract = {For checking the temporal behaviour of embedded systems, realtime scheduling analysis based on abstract, formal models is a wellestablished method. A major difﬁculty for such analytical models in practical usecases is the nontrivial representation of a real implementation model. To overcome this limitation we propose a formal mapping of a concurrent, objectoriented, executable implementation model with explicit shared resources to a realtime task network with functional extensions. The mapping starts from a C++ subset and maps the functional behaviour based on externally observable synchronisation events. The proposed mapping allows to check the implementation model against functional and temporal requirements, like local and endtoend deadlines.},
owner = {guenter},
keywords = {uniol2010sesdamm},
timestamp = {2011.05.04} } 
[inproceedings] bibtexA. Baumgart, P. Reinkemeier, A. Rettberg, I. Stierand, E. Thaden, und R. Weber, "A modelbased design methodology with contracts to enhance the development process of safetycritical systems, pp. 5970.
@InProceedings{ baumgart2010,
author = {Baumgart, Andreas and Reinkemeier, Philipp and Rettberg, Achim and Stierand, Ingo and Thaden, Eike and Weber, Raphael},
title = {A modelbased design methodology with contracts to enhance the development process of safetycritical systems},
booktitle = {Proceedings of the 8th IFIP WG 10.2 international conference on Software technologies for embedded and ubiquitous systems},
year = {2010},
series = {SEUS'10},
pages = {5970},
address = {Berlin, Heidelberg},
publisher = {SpringerVerlag},
abstract = {In this paper a new methodology to support the development process of safetycritical systems with contracts is described. The metamodel of Heterogeneous Rich Component (HRC) is extended to a Common System MetaModel (CSM) that benefits from the semantic foundation of HRC and provides analysis techniques such as compatibility checks or refinement analyses. The idea of viewpoints, perspectives, and abstraction levels is discussed in detail to point out how the CSM supports separation of concerns. An example is presented to detail the transition concepts between models. From the example we conclude that our approach proves valuable and supports the development process.},
acmid = {1927894},
isbn = {364216255X, 9783642162558},
location = {Waidhofen/Ybbs, Austria},
numpages = {12},
owner = {guenter},
keywords = {uniol2010sesdamm},
timestamp = {2011.05.04} } 
[inproceedings] bibtexP. Bhaduri und I. Stierand, "A Proposal for Realtime Interfaces in SPEEDS.
@InProceedings{ bhaduri2010,
author = {Bhaduri, Purandar and Stierand, Ingo},
title = {{A Proposal for Realtime Interfaces in SPEEDS}},
booktitle = {13th Conference on Design, Automation and Test (DATE)},
year = {2010},
month = mar, abstract = {The SPEEDS project is aimed at making rich components models (RCM) into a mature framework in all phases of the design of complex distributed embedded systems. The RCM model is required to be expressive enough to cover the entire development process from requirements to code through design, and also capture both functional and nonfunctional aspects. In this paper we propose a languagebased framework for realtime component interfaces in SPEEDS that is suitable at the ECU layer when a target processor has been identiﬁed, and WCET analysis done. We assume a discrete time model.},
owner = {guenter},
keywords = {uniol2010sesdamm},
timestamp = {2011.05.04} } 
[inproceedings] bibtexW. Damm, H. Dierks, J. Oehlerking, und A. Pnueli, "Towards Component Based Design of Hybrid Systems: Safety and Stability, pp. 96143.
@InProceedings{ dammpnueli10,
author = {Werner Damm and Henning Dierks and Jens Oehlerking and Amir Pnueli},
title = {Towards Component Based Design of Hybrid Systems: Safety and Stability},
booktitle = {Time for Verification: Essays in Meory of Amir Pnueli},
year = {2010},
editor = {Zohar Manna and Doron Peled},
volume = {6200},
series = {Lecture Notes in Computer Science (LNCS)},
pages = {96143},
abstract = {We propose a library based incremental design methodology for constructing hybrid controllers from a component library of models of hybrid controllers, such that global safety and stability properties are preserved. To this end, we propose hybrid interface specifications of components characterizing plant regions for which safety and stability properties are guaranteed, as well as exception mechanisms allowing safe and stabilitypreserving transfer of control whenever the plant evolves towards the boundary of controllable dynamics. We then propose a composition operator for constructing hybrid automata from a library of such precharacterized components supported by compositional and automatable proofs of hybrid interface specifications. },
access = {open},
bibtex = {damm.pnueli10.bib},
editors = {Zohar Manna and Doron A. Peled},
file = {damm.pnueli10.pdf:damm.pnueli10.pdf:PDF},
keywords = {uniol2010sesdamm},
subproject = {H3} } 
[inbook] bibtexW. Damm, R. Achatz, K. Beetz, M. Broy, H. Daembkes, K. Grimm, und P. Liggesmeyer, "Nationale Roadmap Embedded Systems, Broy, M. ., Ed., pp. 67+.
@InBook{ 2010cps..book...67d, pages = {67+},
title = {{Nationale Roadmap Embedded Systems}},
year = {2010},
editor = {{Broy, M.}},
author = {Damm, W. and Achatz, R. and Beetz, K. and Broy, M. and Daembkes, H. and Grimm, K. and Liggesmeyer, P.},
booktitle = {CyberPhysical Systems, acatech DISKUTIERT, Volume 0.~ISBN 9783642144981.~SpringerVerlag Berlin Heidelberg, 2010, p.~67},
doi = {10.1007/9783642149016_5},
owner = {guenter},
keywords = {uniol2010sesdamm},
timestamp = {2011.05.12} } 
[inproceedings] bibtexM. Fränzle, T. Gezgin, H. Hungar, S. Puch, und G. Sauter, "Using Guided Simulation to Assess Driver Assistance Systems.
@InProceedings{ fgh10b,
author = {Fränzle, Martin and Gezgin, Tayfun and Hungar, Hardi and Puch, Stefan and Sauter, Gerald},
title = {Using Guided Simulation to Assess Driver Assistance Systems},
booktitle = {Proc. FORMS/FORMAT 2010},
year = {2010},
editor = {Schnieder, E. and Tarnai, G.},
abstract = {The goal of our approach is the modelbased prediction of the effects of driver assistance systems. Starting with the integration of a computer model of the driver of a car into a simulation environment, we face the problem of analysing the emergent effects of a complex system with discrete, numeric and probabilistic components. In particular, it is difficult to assess the probability of rare events, though we are specifically interested in critical situations which will be infrequent for any reasonable system. For that purpose, we use a quantitative logic which enables us to specify criticality and other properties of simulation runs. An online evaluation of the logic permits us to define a procedure which guides the simulation towards critical situations and allows to estimate the risk of connected with the introduction of the assistance system.},
keywords = {ADAS, cognitive Model, HLA, HLAObserver, IEEE 15162000, LTL, uniol2010sesdamm},
owner = {guenter},
timestamp = {2011.05.10} } 
[inproceedings] bibtexJ. Gacnik, H. Jost, F. Köster, und M. Fränzle, "The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge.
@InProceedings{ jost10c,
author = {Jan Gacnik and Henning Jost and Frank Köster and Martin Fränzle},
title = {The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge},
booktitle = {Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010)},
year = {2010},
keywords = {uniol2010sesdamm},
editor = {Eckehard Schnieder and G\'{e}za Tarnai},
note = {ausgezeichnet mit dem Best Paper Award} } 
[inproceedings] bibtexH. Jost, "Automating the Risk and Hazard Analysis via Generic Domain Concepts in Formal Ontologies.
@InProceedings{ jost10a,
author = {Henning Jost},
title = {Automating the Risk and Hazard Analysis via Generic Domain Concepts in Formal Ontologies},
booktitle = {Reliability, Risk and Safety  Back to the Future, European Safety and Reliability Conference (ESREL 2010)},
year = {2010},
keywords = {uniol2010sesdamm},
editor = {Ben J.M. Ale and Ioannis A. Papazoglou and Enrico Zio} } 
[inproceedings] bibtexH. Jost, S. Köhler, S. Häusler, J. Gacnik, A. Hahn, F. Köster, und K. Lemmer, "Supporting Qualification  Safety Standard Compliant Process Planning and Monitoring.
@InProceedings{ jost10b,
author = {Henning Jost and Silke Köhler and Stefan {Häusler} and Jan Gacnik and Axel Hahn and Frank {Köster} and Karsten Lemmer},
title = {Supporting Qualification  Safety Standard Compliant Process Planning and Monitoring},
booktitle = {Proceedings 2010 IEEE Symposium on Product Compliance Engineering (PSES 2010)},
keywords = {uniol2010sesdamm},
year = {2010} } 
[inproceedings] bibtex  Dokument aufrufenT. Kerstan und M. Oertel, "Design of a realtime optimized emulation method, pp. 646649.
@InProceedings{ kerstan:2010:dro:1870926.1871079,
author = {Kerstan, Timo and Oertel, Markus},
title = {Design of a realtime optimized emulation method},
booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe},
year = {2010},
series = {DATE '10},
pages = {646649},
address = {3001 Leuven, Belgium, Belgium},
publisher = {European Design and Automation Association},
acmid = {1871079},
isbn = {9783981080162},
location = {Dresden, Germany},
numpages = {4},
owner = {guenter},
timestamp = {2011.05.12},
keywords = {uniol2010sesdamm},
url = {http://portal.acm.org/citation.cfm?id=1870926.1871079} } 
[inproceedings] bibtexE. Thaden, H. Lipskoch, A. Metzner, und I. Stierand, "Exploiting Gaps in FixedPriority Preemptive Schedules for Task Insertion.
@InProceedings{ thaden2010,
author = {Eike Thaden and Henrik Lipskoch and Alexander Metzner and Ingo Stierand},
title = {Exploiting Gaps in FixedPriority Preemptive Schedules for Task Insertion},
booktitle = {Proceedings of the 16th IEEE International Conference on Embedded and RealTime Computing Systems and Applications (RTCSA)},
year = {2010},
abstract = {This paper addresses the problem of assigning tasks to embedded control units. The units are considered to be connected via a bus, and tasks may already be deployed onto the units. To save costs, the objective is to insert as many new tasks onto the system as possible. In this setting, to support early design decisions, we present an approximative and fast preanalysis of the system. We introduce sparetime analysis and the analysis of maximal allowed worstcase execution time to simplify the problem and to achieve a fast solving algorithm, which we implement as mixedinteger linear problem. We conduct experiments to investigate the scalability of the approach with the result that for input sizes of up to 160 tasks with up to 50% notyetdeployed tasks a solution is found in many cases within reasonable time, our machine needs in the average case 150s. With a reference example, taken from literature, we compare our approach with a similar method and show that our approach is faster.},
access = {restricted},
keywords = {uniol2010sesdamm},
bibtex = {thaden.rtcsa10.bib},
file = {thaden.rtcsa10.pdf:thaden.rtcsa10.pdf:PDF},
subproject = {R2} } 
[inproceedings] bibtexJ. Thyssen, D. Ratiu, W. Schwitzer, A. Harhurin, M. Feilkas, und E. Thaden, "A System for Seamless Abstraction Layers for Modelbased Development of Embedded Software.
@InProceedings{ thyssen2010abstractionlayers,
author = {Thyssen, Judith and Ratiu, Daniel and Schwitzer, Wolfgang and Harhurin, Alexander and Feilkas, Martin and Thaden, Eike},
title = {A System for Seamless Abstraction Layers for Modelbased Development of Embedded Software},
booktitle = {Proceedings of Envision 2020 Workshop},
year = {2010},
publisher = {Bonner Köllen Verlag},
abstract = {Modelbased development aims at reducing the complexity of software development by the pervasive use of adequate models throughout the whole development process starting from early phases up to implementation. In this paper we present a conceptual framework to holistically classify developed models along different levels of abstraction. We do this by designing adequate abstractions for different development stages while ignoring the information that is not relevant at a particular development step or for a certain stakeholder. The abstraction is achieved in terms of the granularity level of the system under study (e. g. system, subsystem, subsubsystem) and in terms of the information that the models contain (e. g. specification of functionality, description of architecture, deployment on specific hardware). We also present the relation between models that describe different perspectives of the system or are at different granularity levels. However, we do not address the process to be followed for building these models.},
isbn = {9783885792536},
issn = {16175468},
owner = {guenter},
keywords = {uniol2010sesdamm},
timestamp = {2011.05.10} } 
[inproceedings] bibtex  Dokument aufrufenT. Toben, B. Westphal, und J. Rakow, "Spotlight Abstraction of Agents and Areas.
@InProceedings{ toben_et_al:dsp:2010:2517,
author = {Tobe Toben and Bernd Westphal and JanHendrik Rakow},
title = {Spotlight Abstraction of Agents and Areas},
booktitle = {Quantitative and Qualitative Analysis of Network Protocols},
year = {2010},
editor = {Bengt Jonsson and Jörg Kreiker and Marta Kwiatkowska},
number = {10051},
series = {Dagstuhl Seminar Proceedings},
address = {Dagstuhl, Germany},
publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik, Germany},
abstract = {We present "spotlight abstraction" as a generic abstraction technique for the analysis of systems comprising an unbounded number of communicating agents. The abstraction principle is heterogeneous in the sense that the behaviour of a finite number of agents is preserved while the others are only abstractly represented. The precision of the abstraction can be tuned by an iterative procedure based on the analysis of counterexamples. Going beyond existing work, we show how to use the spotlight principle for analysing systems where the physical position of agents is relevant. To this end, we put the spotlight on areas rather than on fixed sets of agents.},
access = {restricted},
bibtex = {toben.dagstuhl10051.bib},
file = {toben.dagstuhl10051.pdf:toben.dagstuhl10051.pdf:PDF},
issn = {18624405},
keywords = {Spotlight Abstraction, Verification, Dynamic Communication Systems, uniol2010sesdamm},
subproject = {S2},
url = {http://drops.dagstuhl.de/opus/volltexte/2010/2517} }
2009

[inproceedings] bibtexM. Baumann, H. Colonius, H. Hungar, F. Köster, M. Langner, A. Lüdtke, C. Möbus, J. Peinke, S. Puch, C. Schiessl, R. Steenken, und L. Weber, "Integrated Modeling for Safe Transportation  Driver modeling and driver experiments, pp. 8499.
@INPROCEEDINGS{Baumann2009,
author = {Baumann, M. and Colonius, H. and Hungar, H. and K{\"o}ster, F. and Langner, M. and L{\"u}dtke, A. and M{\"o}bus, C. and Peinke, J. and Puch, S. and Schiessl, C. and Steenken, R. and Weber, L.},
title = {Integrated Modeling for Safe Transportation  Driver modeling and driver experiments},
booktitle = {Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung für Fahrermodellierung},
year = {2009},
editor = {T. Jürgensoh and H. Kolrep},
number = {28},
series = {FortschrittBericht VDI in der Reihe 22 (MenschMaschineSysteme)},
pages = {8499},
address = {Düsseldorf},
publisher = {VDIVerlag},
owner = {luedtke},
timestamp = {2009.11.02} } 
[article] bibtexE. Bode, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, J. Rakow, R. Wimmer, und B. Becker, "Compositional Dependability Evaluation for STATEMATE, pp. 274292
@ARTICLE{Bode2009,
author = {Bode, E. and Herbstritt, M. and Hermanns, H. and Johr, S. and Peikenkamp, T. and Pulungan, R. and Rakow, J. and Wimmer, R. and Becker, B.},
title = {Compositional Dependability Evaluation for STATEMATE},
journal = {Software Engineering, IEEE Transactions on},
year = {2009},
volume = {35},
pages = {274292},
number = {2},
abstract = {Software and system dependability is getting ever more important in embedded system design. Current industrial practice of modelbased analysis is supported by statetransition diagrammatic notations such as Statecharts. Stateoftheart modelling tools like STATEMATE support safety and failureeffect analysis at design time, but restricted to qualitative properties. This paper reports on a (plugin) extension of STATEMATE enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuoustime Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safetycritical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a highspeed train signalling system where the tool has been applied successfully.},
access = {restricted},
bibtex = {boede.jse09.bib},
keywords = {checking, ctmc, mdp, model, stochastic},
pdf = {boede.jse09.pdf},
priority = {2},
subprojects = {S3} } 
[inproceedings] bibtexM. Büker, A. Metzner, und I. Stierand, "Testing RealTime Task Networks with Functional Extensions Using ModelChecking.
@INPROCEEDINGS{BukerMetznerStierand2009,
author = {B{\"u}ker, Matthias and Metzner, Alexander and Stierand, Ingo},
title = {Testing RealTime Task Networks with Functional Extensions Using ModelChecking},
booktitle = {14th International Conference on Emerging Technologies and Factory Automation (ETFA'09)},
year = {2009} } 
[inproceedings] bibtexW.~Damm, T.~Peikenkamp, und B.~Josko, "Contract Based ISO CD 26262 Safety Analysis.
@INPROCEEDINGS{DPJ09,
author = {W.~Damm and T.~Peikenkamp and B.~Josko},
title = {{Contract Based ISO CD 26262 Safety Analysis}},
booktitle = {{SAE World Congress  Session on SafetyCritical Systems}},
year = {2009},
owner = {guenter},
timestamp = {2011.05.12} } 
[inproceedings] bibtexH. Dierks, A. Metzner, und I. Stierand, "Efficient ModelChecking for RealTime Task Networks.
@INPROCEEDINGS{Dierks2009,
author = {Dierks, Henning and Metzner, Alexander and Stierand, Ingo},
title = {Efficient ModelChecking for RealTime Task Networks},
booktitle = {6th International Conference on Embedded Software and Systems},
year = {2009},
month = may, __markedentry = {[guenter]},
owner = {guenter},
timestamp = {2011.05.04} } 
[inproceedings] bibtexF. Frische, T. Mistrzyk, und A. Lüdtke, "Detection of Pilot Errors in Data by combining Task Modeling and Model Checking.
@INPROCEEDINGS{Frische2009,
author = {Frische, F. and Mistrzyk, T. and L{\"u}dtke, A.},
title = {Detection of Pilot Errors in Data by combining Task Modeling and Model Checking},
booktitle = {Proceedings INTERACT 2009, 12th IFIP TC13 Conference in HumanComputer Interaction, Part I},
year = {2009},
series = {LNCS 5726},
publisher = {Springer},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexJ. G. c, H. Jost, D. Beisel, J. Rataj, und F. Köster, "DeSCAS Design Process Model for Automotive Systems  Development Streams and Ontologies, p. 10.
@INPROCEEDINGS{Jost09a,
author = {Jan Ga\v{c}nik and Henning Jost and Daniel Beisel and J{\"u}rgen Rataj and Frank K{\"o}ster},
title = {DeSCAS Design Process Model for Automotive Systems  Development Streams and Ontologies},
booktitle = {SafetyCritical Systems 2009},
year = {2009},
number = {SP2222},
series = {Special Publications},
pages = {10 pages},
publisher = {SAE International} } 
[inproceedings] bibtexJ. G. c, H. Jost, F. Köster, J. Rataj, K. Lemmer, W. Damm, M. Fränzle, und E. Schnieder, "DeSCAS  Formale Ontologien zur Verwebung von interdisziplinären Entwicklungsprozessen, pp. 449452 (langfassung auf cd.
@INPROCEEDINGS{Jost09b,
author = {Jan Ga\v{c}nik and Henning Jost and Frank K{\"o}ster and J{\"u}rgen Rataj and Karsten Lemmer and Werner Damm and Martin Fr{\"a}nzle and Eckehard Schnieder},
title = {DeSCAS  Formale Ontologien zur Verwebung von interdisziplin{\"a}ren Entwicklungsprozessen},
booktitle = {AUTOMATION 2009},
year = {2009},
number = {2067},
series = {VDIBerichte},
pages = {449  452 (Langfassung auf CDROM: 12 Seiten)},
publisher = {VDI Wissensforum GmbH} } 
[inproceedings] bibtexA. Lüdtke, "New Requirements for Modelling how Humans Succeed and Fail in Complex Traffic Scenarios.
@INPROCEEDINGS{Ludtke2009c,
author = {L{\"u}dtke, A.},
title = {New Requirements for Modelling how Humans Succeed and Fail in Complex Traffic Scenarios},
booktitle = {Proceedings of the 7th Working Conference on Human Error, Safety and Systems Development Systems Development (HESSD)},
year = {2009},
editor = {J. Vanderdonckt and P. Palanque},
series = {LNCS},
publisher = {Springer Verlag},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexA. Lüdtke und JP. Osterloh, "Simulating Perceptive Processes of Pilots to Support System Design.
@INPROCEEDINGS{Ludtke2009b,
author = {L{\"u}dtke, A. and Osterloh, JP.},
title = {Simulating Perceptive Processes of Pilots to Support System Design},
booktitle = {Proceedings INTERACT 2009, 12th IFIP TC13 Conference in HumanComputer Interaction, Part I},
year = {2009},
series = {LNCS 5726},
publisher = {Springer},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexA. Lüdtke, J. P. Osterloh, T. Mioch, F. Rister, und R. Looije, "Cognitive Modelling of Pilot Errors and Error Recovery in Flight Management Tasks.
@INPROCEEDINGS{Ludtke2009a,
author = {L{\"u}dtke, A. and Osterloh, J.P. and Mioch, T. and Rister, F. and Looije, R.},
title = {Cognitive Modelling of Pilot Errors and Error Recovery in Flight Management Tasks},
booktitle = {Proceedings of the 7th Working Conference on Human Error, Safety and Systems Development Systems Development (HESSD)},
year = {2009},
editor = {J. Vanderdonckt and P. Palanque},
series = {LNCS},
publisher = {Springer Verlag},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexA. Lüdtke, L. Weber, J. Osterloh, und B. Wortelen, "Modeling Pilot and Driver Behavior for Human Error Simulation, pp. 403412.
@INPROCEEDINGS{LWOW2009,
author = {L{\"{u}}dtke, Andreas and Weber, Lars and Osterloh, JanPatrick and Wortelen, Bertram},
title = {Modeling Pilot and Driver Behavior for Human Error Simulation},
booktitle = {Proceedings of the HCI International 2009},
year = {2009},
pages = {403412},
address = {San Diego},
abstract = {In order to reduce human errors in the interaction with in safety criti cal assistance systems it is crucial to consequently include the characteristics of the human operator already in the early phases of the design process. In this pa per we present a cognitive architecture for simulating manmachine interaction in the aeronautics and automotive domain. Though both domains have their own characteristics we think that it is possible to apply the same core architec ture to support pilot as well driver centered design of assistance systems. This text shows how phenomena relevant in the automobile or aviation environment can be integrated in the same cognitive architecture.},
keywords = {cognitive architecture, drivers, human error simulation, pilots},
owner = {guenter},
timestamp = {2011.05.10} } 
[article] bibtexR. Passerone, I. B. Hafaiedh, S. Graf, A. Benveniste, D. Cancila, A. Cuccuru, S. Gerard, F. Terrier, W. Damm, A. Ferrari, L. Mangeruca, B. Josko, T. Peikenkamp, und A. SangiovanniVincentelli, "Metamodels in Europe: Languages, Tools, and Applications, pp. 3853
@ARTICLE{10.1109/MDT.2009.64,
author = {Roberto Passerone and Imene Ben Hafaiedh and Susanne Graf and Albert Benveniste and Daniela Cancila and Arnaud Cuccuru and Sebastien Gerard and Francois Terrier and Werner Damm and Alberto Ferrari and Leonardo Mangeruca and Bernhard Josko and Thomas Peikenkamp and Alberto SangiovanniVincentelli},
title = {Metamodels in Europe: Languages, Tools, and Applications},
journal = {IEEE Design and Test of Computers},
year = {2009},
volume = {26},
pages = {3853},
address = {Los Alamitos, CA, USA},
doi = {http://doi.ieeecomputersociety.org/10.1109/MDT.2009.64},
issn = {07407475},
owner = {guenter},
publisher = {IEEE Computer Society},
timestamp = {2011.05.12} } 
[inproceedings] bibtex  Dokument aufrufenG. Sauter, H. Dierks, M. Fränzle, und M. R. Hansen, "Lightweight hybrid model checking facilitating online prediction of temporal properties, pp. 2022.
@INPROCEEDINGS{SauterEA:NWPT09,
author = {Sauter, Gerald and Dierks, Henning and Fr{\"{a}}nzle, Martin and Hansen, Michael R.},
title = {Lightweight hybrid model checking facilitating online prediction of temporal properties},
booktitle = {Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09},
year = {2009},
pages = {2022},
address = {Kgs. Lyngby, Denmark},
publisher = {Danmarks Tekniske Universitet},
note = {\url{http://imost.informatik.unioldenburg.de}},
url = {http://imost.informatik.unioldenburg.de/download/RobustMonitoringNWPT09.pdf} } 
[phdthesis] bibtex  Dokument aufrufenT. Toben, "Analysis of Dynamic Evolution Systems by Spotlight Abstraction Refinement,".
@PHDTHESIS{Toben2009_phd,
author = {Tobe Toben},
title = {Analysis of Dynamic Evolution Systems by Spotlight Abstraction Refinement},
school = {Carl von Ossietzky Universit{\"a}t Oldenburg, Germany},
year = {2009},
month = feb, note = {urn:nbn:de:gbv:715oops8760},
url = {http://oops.unioldenburg.de/volltexte/2009/876/} } 
[article] bibtexL. Weber, M. Baumann, A. Luedtke, und R. Steenken, "Modellierung von Entscheidungen beim Einfädeln auf die Autobahn
@ARTICLE{Weber2009,
author = {Weber, L. and Baumann, M. and Luedtke, A. and Steenken, R.},
title = {Modellierung von Entscheidungen beim Einf{\"a}deln auf die Autobahn},
journal = {to appear: FortschrittsBerichte VDI: Der Mensch im Mittelpunkt technischer Systeme. 8. Berliner Werkstatt MenschMaschineSysteme},
year = {2009},
owner = {LarsW},
timestamp = {2009.09.18} } 
[inproceedings] bibtexB. Wortelen und A. Lüdtke, "Ablauffähige Modellierung des Einflusses von Ereignishäufigkeiten auf die Aufmerksamkeitsverteilung von Autofahrern, pp. 8085.
@INPROCEEDINGS{Wortelen2009,
author = {Wortelen, B. and L{\"u}dtke, A.},
title = {Ablauff{\"a}hige Modellierung des Einflusses von Ereignish{\"a}ufigkeiten auf die Aufmerksamkeitsverteilung von Autofahrern},
booktitle = {Der Mensch im Mittelpunkt technischer Systeme, 8. Berliner Werkstatt, MenschMaschineSysteme, ZMMS Spektrum Band 22},
year = {2009},
editor = {A. Lichtenstein and C. St{\"o}{\ss}el and C. Clemens},
number = {29},
series = {FortschrittBerichte VDI, Reihe 22 MenschMaschineSysteme},
pages = {8085},
address = {D{\"u}sseldorf},
publisher = {VDI Verlag},
note = {ISBN 9783183029228, ISSN 1439958X},
owner = {luedtke},
timestamp = {2009.11.02} } 
[proceedings] bibtexProceedings of the First Workshop on Certification of SafetyCritical Software Controlled Systems (SafeCert 2008).
@PROCEEDINGS{HuHu09a, title = {Proceedings of the First Workshop on Certification of SafetyCritical Software Controlled Systems (SafeCert 2008)},
year = {2009},
editor = {Michaela Huhn and Hardi Hungar},
volume = {238},
number = {4},
series = {Electronic Notes in Theoretical Computer Science},
owner = {hardi},
timestamp = {2010.01.13} }
2008

[inproceedings] bibtexH. Hungar, "Positionsstatement: Zertifizierungsargumentationen mit mathematischer Präzision, pp. 339340.
@INPROCEEDINGS{DBLP:conf/se/Hungar08,
author = {Hardi Hungar},
title = {Positionsstatement: Zertifizierungsargumentationen mit mathematischer Pr{\"a}zision},
booktitle = {Software Engineering (Workshops)},
year = {2008},
pages = {339340},
bibsource = {DBLP, http://dblp.unitrier.de},
crossref = {DBLP:conf/se/2008w} } 
[inproceedings] bibtexH. Hungar und E. Reyzl, "SoftwareEntwicklung und Zertifizierung im Umfeld sicherheitskritischer und hochverfügbarer Systeme: Bedeutung modellbasierter und formaler Ansätze für effiziente Entwicklung und Zertifizierung, pp. 291294.
@INPROCEEDINGS{DBLP:conf/se/HungarR08,
author = {Hardi Hungar and Erwin Reyzl},
title = {SoftwareEntwicklung und Zertifizierung im Umfeld sicherheitskritischer und hochverf{\"u}gbarer Systeme: Bedeutung modellbasierter und formaler Ans{\"a}tze f{\"u}r effiziente Entwicklung und Zertifizierung},
booktitle = {Software Engineering},
year = {2008},
pages = {291294},
bibsource = {DBLP, http://dblp.unitrier.de},
crossref = {DBLP:conf/se/2008} } 
[inproceedings] bibtexH. Hungar und E. Reyzl, "Ergebnisse des Workshops "SoftwareEntwicklung und Zertifizierung im Umfeld sicherheitskritischer und hochverfügbarer Systeme", pp. 345349.
@INPROCEEDINGS{DBLP:conf/se/HungarR08b,
author = {Hardi Hungar and Erwin Reyzl},
title = {Ergebnisse des Workshops "SoftwareEntwicklung und Zertifizierung im Umfeld sicherheitskritischer und hochverf{\"u}gbarer Systeme"},
booktitle = {Software Engineering (Workshops)},
year = {2008},
pages = {345349},
bibsource = {DBLP, http://dblp.unitrier.de},
crossref = {DBLP:conf/se/2008w} } 
[incollection] bibtexM. Baumann, H. Colonius, H. Hungar, F. Köster, M. Langner, A. Lüdtke, C. Möbus, J. Peinke, S. Puch, C. Schiessl, R. Steenken, und L. Weber, "Integrated Modelling for Safe Transportation  Driver modeling and driver experiments, Jürgensohn, T. und Kolrep, H., Eds.
@INCOLLECTION{BaumannColonius08,
author = {Baumann, M. and Colonius, H. and Hungar, H. and K\"oster, F. and Langner, M. and L\"udtke, A. and M\"obus, C. and Peinke, J. and Puch, S. and Schiessl, C. and Steenken, R. and Weber, L.},
title = {Integrated Modelling for Safe Transportation  Driver modeling and driver experiments},
booktitle = {Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung f{\"}ur Fahrzeugsmodellierung},
publisher = {VDI Verlag},
year = {2008},
editor = {T. J\"{u}rgensohn and H. Kolrep},
address = {D\"usseldorf},
endnotereftype = {Book Section},
shorttitle = {Integrated Modelling for Safe Transportation  Driver modeling and driver experiments} } 
[conference] bibtexR. Buschermoehle und J. Oelerink, "Rich Meta Object Facility as formal integration platform: Syntax, Semantics, and Implementation.
@CONFERENCE{RBJO2008,
author = {Ralf Buschermoehle and Joerg Oelerink},
title = {Rich Meta Object Facility as formal integration platform: Syntax, Semantics, and Implementation},
booktitle = {Innovations in Systems and Software Engineering},
year = {2008},
volume = {4},
number = {3},
publisher = {Springer Verlag} } 
[techreport] bibtexE. Böde, T. Peikenkamp, J. Rakow, und S. Wischmeyer, "Model Based Importance Analysis for Minimal Cut Sets,".
@TECHREPORT{atr29,
author = {Eckard B{\"o}de and Thomas Peikenkamp and Jan Rakow and Samuel Wischmeyer},
title = {Model Based Importance Analysis for Minimal Cut Sets},
institution = {SFB/TR 14 AVACS},
year = {2008},
type = {Reports of SFB/TR 14 AVACS},
number = {29},
month = {Apr},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = { In this report we show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute the probability of reaching a safetycritical state and to what extent certain fault configurations contribute to this probability. },
access = {open},
bibtex = {atr029.bib},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
pdf = {avacs_technical_report_029.pdf},
series = {ATR},
subproject = {S3} } 
[inproceedings] bibtexE. Böde, T. Peikenkamp, J. Rakow, und S. Wischmeyer, "Model Based Importance Analysis for Minimal Cut Sets, pp. 303317.
@INPROCEEDINGS{atva08,
author = {Eckard B{\"o}de and Thomas Peikenkamp and Jan Rakow and Samuel Wischmeyer},
title = {Model Based Importance Analysis for Minimal Cut Sets},
booktitle = {Automated Technology for Verification and Analysis, 6th International Symposium ATVA 2008, Seoul, Korea},
year = {2008},
volume = {5311},
series = {LNCS},
pages = {303317},
abstract = {We show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute to what extent certain fault con?gurations contribute to the probability of reaching a safetycritical state.},
access = {restricted},
bibtex = {boede.atva2008.bib},
pdf = {boede.atva2008.pdf},
subproject = {S3} } 
[inproceedings] bibtexF. Frische, T. Mistrzyk, und A. Lüdtke, "Modellierung und Analyse von Pilotenverhalten in FlugzeugCockpits.
@INPROCEEDINGS{Frische2008,
author = {Frische, F. and Mistrzyk, T. and L{\"u}dtke, A.},
title = {Modellierung und Analyse von Pilotenverhalten in FlugzeugCockpits},
booktitle = {.50. Sitzung des Fachausschusses Anthropotechnik der Deutschen Gesellschaft f\{"u}r Luft und Raumfahrt, Beitr{\"a}ge der Ergonomie zur MenschSystemIntegration},
year = {2008},
editor = {M. Grandt and A. Bauch},
number = {200804},
series = {DGLRBericht},
address = {Bonn},
publisher = {DGLR e.V.},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexJ. Gacnik, H. Jost, D. Beisel, und F. Köster, "DeSCAS  Design Process for the Development of SafetyCritical Advanced Driver Assistance Systems, pp. 103110.
@INPROCEEDINGS{FORMS08,
author = {Jan Gacnik and Henning Jost and Daniel Beisel and Frank K{\"o}ster},
title = {DeSCAS  Design Process for the Development of SafetyCritical Advanced Driver Assistance Systems},
booktitle = {Formal Methods for Automation and Safety in Railway and Automotive Systems},
year = {2008},
editor = {Ga Tarnai and Eckehard Schnieder},
pages = {103110} } 
[inproceedings] bibtexA. Lüdtke, "Analyse kognitiver Aspekte der Kommunikation im Flugzeugcockpit.
@INPROCEEDINGS{Ludtke2008a,
author = {L{\"u}dtke, A.},
title = {Analyse kognitiver Aspekte der Kommunikation im Flugzeugcockpit},
booktitle = {Workshop Proceedings der Tagungen Mensch & Computer 2008, DeLFI 2008 und Cognitive Design 2008},
year = {2008},
editor = {U. Lucke and M. C. Kindsmüller and S. Fischer and M. Herczeg and S. Seehusen},
address = {Berlin},
publisher = {Logos Verlag},
note = {ISBN 9783832520076},
owner = {luedtke},
timestamp = {2009.11.02} } 
[article] bibtexA. Lüdtke, "Analyse von Fahrer und Pilotenfehlern mit integrierten MenschMaschineUmgebung Modellen, pp. 2430
@ARTICLE{Ludtke2008,
author = {L{\"u}dtke, A.},
title = {Analyse von Fahrer und Pilotenfehlern mit integrierten MenschMaschineUmgebung Modellen},
journal = {icom},
year = {2008},
volume = {7},
pages = {2430},
number = {1},
owner = {luedtke},
timestamp = {2009.11.02} } 
[book] bibtexE. R. Olderog und H. Dierks, RealTime Systems: Formal Specification and Automatic Verification
@BOOK{OD08, title = {RealTime Systems: Formal Specification and Automatic Verification},
publisher = {Cambridge University Press},
year = {2008},
author = {E.R. Olderog and H. Dierks},
note = {ISBN13: 9780521883337} } 
[inproceedings] bibtexJ. P. Osterloh und A. Lüdtke, "Analyzing the Ergonomics of Aircraft Cockpits Using Cognitive Models, p. 10.
@INPROCEEDINGS{Osterloh2008,
author = {Osterloh, J.P. and L{\"u}dtke, A.},
title = {Analyzing the Ergonomics of Aircraft Cockpits Using Cognitive Models},
booktitle = {Proceedings of the 2nd International Conference on Applied Human Factors and Ergonomic (AHFE)},
year = {2008},
editor = {W. Karowski and G. Salvendy},
pages = {10 pages},
publisher = {USA Publishing},
note = {CD Rom. ISBN 9781606437124},
owner = {luedtke},
timestamp = {2009.11.02} } 
[inproceedings] bibtexT. Toben, "Counterexample Guided Spotlight Abstraction Refinement, pp. 2136.
@INPROCEEDINGS{Toben2008,
author = {Tobe Toben},
title = {Counterexample Guided Spotlight Abstraction Refinement},
booktitle = {Proceedings of the 28th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2008)},
year = {2008},
editor = {K. Suzuki and T. Higashino and K. Yasumoto and K. ElFakih},
volume = {5048},
series = {LNCS},
pages = {2136},
address = {Tokyo, Japan},
month = jun, publisher = {SpringerVerlag} } 
[inproceedings] bibtexT. Toben und B. Westphal, "Concurrent LSC Verification, pp. 95111.
@INPROCEEDINGS{TobenWestphal2006a,
author = {Tobe Toben and Bernd Westphal},
title = {Concurrent LSC Verification},
booktitle = {Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS'05)},
year = {2006},
editor = {Ranko Lazic and Rajagopal Nagarajan},
volume = {145},
series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
pages = {95111},
address = {Warwick, UK},
month = jan, publisher = {Elsevier B. V.} } 
[inproceedings] bibtexL. Urbas, S. Leuchter, und A. Lüdtke, "Modellierung und Simulation von Teams in sicherheitskritischen MenschMaschineSystemen.
@INPROCEEDINGS{Urbas2008,
author = {Urbas, L. and Leuchter, S. and L{\"u}dtke, A.},
title = {Modellierung und Simulation von Teams in sicherheitskritischen MenschMaschineSystemen},
booktitle = {Workshop Proceedings der Tagungen Mensch & Computer 2008, DeLFI 2008 und Cognitive Design 2008},
year = {2008},
editor = {U. Lucke and M. C. Kindsm{\"a}ller and S. Fischer and M. Herczeg and S. Seehusen},
address = {Berlin},
publisher = {Logos Verlag},
note = {ISBN 9783832520076},
owner = {luedtke},
timestamp = {2009.11.02} } 
[phdthesis] bibtex  Dokument aufrufenB. Westphal, "Specification and Verification of Dynamic Topology Systems,".
@PHDTHESIS{Westphal2008_phd,
author = {Bernd Westphal},
title = {Specification and Verification of Dynamic Topology Systems},
school = {Carl von Ossietzky Universit{\"a}t Oldenburg, Germany},
year = {2008},
month = may, note = {urn:nbn:de:gbv:715oops7900},
url = {http://oops.unioldenburg.de/volltexte/2008/790/} } 
[proceedings] bibtexTools for the Modelbased Development of Certifiable, Dependable Systems, 10.06.  15.06.2007.
@PROCEEDINGS{DBLP:conf/dagstuhl/2007P7241, title = {Tools for the Modelbased Development of Certifiable, Dependable Systems, 10.06.  15.06.2007},
year = {2008},
editor = {Michaela Huhn and Hardi Hungar and Doron Peled},
volume = {07241},
series = {Dagstuhl Seminar Proceedings},
publisher = {Internationales Begegnungs und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany},
bibsource = {DBLP, http://dblp.unitrier.de},
booktitle = {Tools for the Modelbased Development of Certifiable, Dependable Systems} }
2007

[inproceedings] bibtexM. Huhn, H. Hungar, und D. Peled, "07241 Summary  Tools for the Modelbased Development of Certifiable, Dependable Systems.
@INPROCEEDINGS{DBLP:conf/dagstuhl/HuhnHP07,
author = {Michaela Huhn and Hardi Hungar and Doron Peled},
title = {07241 Summary  Tools for the Modelbased Development of Certifiable, Dependable Systems},
booktitle = {Tools for the Modelbased Development of Certifiable, Dependable Systems},
year = {2007},
bibsource = {DBLP, http://dblp.unitrier.de},
crossref = {DBLP:conf/dagstuhl/2007P7241},
ee = {http://drops.dagstuhl.de/opus/volltexte/2008/1405} } 
[inproceedings] bibtexB. Wachter und B. Westphal, "The Spotlight Principle. On Combining ProcessSummarising State Abstractions, pp. 182198.
@INPROCEEDINGS{WachterWestphal2007,
author = {Bj{\"o}rn Wachter and Bernd Westphal},
title = {The Spotlight Principle. On Combining ProcessSummarising State Abstractions},
year = {2007},
pages = {182198},
crossref = {ProcVMCAI2007} } 
[inproceedings] bibtex  Dokument aufrufenJ. Bauer, W. Damm, T. Toben, und B. Westphal, "Verification and Synthesis of OCL Constraints via Topology Analysis: A Case Study.
@INPROCEEDINGS{BauerDammTobenWestphal2007,
author = {J{\"o}rg Bauer and Werner Damm and Tobe Toben and Bernd Westphal},
title = {Verification and Synthesis of OCL Constraints via Topology Analysis: A Case Study},
booktitle = {Applications of Graph Transformations with Industrial Relevance Third International Symposium, AGTIVE 2007, Proceedings of Selected and Invited Papers, Schlosshotel am Bergpark, Wilhelmsh{\"o}he, Kassel, Germany, October 10  12, 2007},
year = {2007},
editor = {Andy Sch{\"u}rr, Manfred Nagl, Albert Z{\"u}ndorf},
month = oct, publisher = {Universit\"{a}t Kassel},
url = {http://www.se.eecs.unikassel.de/se/fileadmin/se/publications/AGTIVE2007Proceedings.pdf} } 
[inproceedings] bibtexJ. Bauer, T. Toben, und B. Westphal, "Mind the Shapes: Abstraction Refinement Via Topology Invariants, pp. 3550.
@INPROCEEDINGS{BauerTobenWestphal2007,
author = {J{\"o}rg Bauer and Tobe Toben and Bernd Westphal},
title = {Mind the Shapes: Abstraction Refinement Via Topology Invariants},
booktitle = {Proceedings of the Fifth International Symposium on Automated Technology for Verification and Analysis (ATVA 2007)},
year = {2007},
editor = {K. S. Namjoshi and T. Yoneda and T. Higashino and Y. Okamura},
volume = {4762},
series = {LNCS},
pages = {3550},
address = {Tokyo, Japan},
month = oct, publisher = {SpringerVerlag} } 
[inproceedings] bibtexS. Blom, J. Calame, B. Lisser, S. Orzan, J. Pang, J. van de Pol, M. Torabi Dashti, und A. Wijs, "Distributed analysis with $\mu$CRL: A compendium of case studies.
@INPROCEEDINGS{BCLOP+07,
author = {Stefan Blom and Jens Calame and Bert Lisser and Simona Orzan and Jun Pang and Jaco {van de Pol} and Mohammad {Torabi Dashti} and Anton Wijs},
title = {Distributed analysis with $\mu${CRL}: A compendium of case studies},
booktitle = {Proc.\ 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems},
year = {2007},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
note = {To appear} } 
[inproceedings] bibtex  Dokument aufrufenW. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, und B. Wirtz, "Exact state set representations in the verification of linear hybrid systems with large discrete statespace, pp. 425440.
@INPROCEEDINGS{DammDHJPPSWW07,
author = {W. Damm and S. Disch and H. Hungar and S. Jacobs and J. Pang and F. Pigorsch and C. Scholl and U. Waldmann and B. Wirtz},
title = {Exact state set representations in the verification of linear hybrid systems with large discrete statespace},
booktitle = {Automated Technology for Verification and Analysis},
year = {2007},
editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura},
volume = {4762},
series = {Lecture Notes in Computer Science},
pages = {425440},
publisher = {Springer},
note = {\url{http://dx.doi.org/10.1007/9783540755968_30}{(c) SpringerVerlag}},
doi = {10.1007/9783540755968_30},
url = {http://dx.doi.org/10.1007/9783540755968_30} } 
[inproceedings] bibtex  Dokument aufrufenW. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, und B. Wirtz, "Automating Verification of Cooperation, Control, and Design in Traffic Applications., pp. 115169.
@INPROCEEDINGS{DammMOOPPSW07,
author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and ErnstR{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz},
title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications.},
booktitle = {Formal Methods and Hybrid RealTime Systems},
year = {2007},
editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
volume = {4700},
series = {Lecture Notes in Computer Science},
pages = {115169},
publisher = {Springer},
note = {\url{http://dx.doi.org/10.1007/9783540752219_6}{(c) SpringerVerlag}},
abstract = {We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of preverified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, modelchecking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.},
doi = {10.1007/9783540752219_6},
url = {http://dx.doi.org/10.1007/9783540752219_6} } 
[incollection] bibtexW. Damm, T. Toben, und B. Westphal, "On the Expressive Power of Live Sequence Charts, Reps, T., Sagiv, M., und Bauer, J., Eds., pp. 225246.
@INCOLLECTION{DammTobenWestphal2007,
author = {Werner Damm and Tobe Toben and Bernd Westphal},
title = {On the Expressive Power of Live Sequence Charts},
booktitle = {Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm},
publisher = {SpringerVerlag},
year = {2007},
editor = {Thomas Reps and Mooly Sagiv and J{\"o}rg Bauer},
number = {4444},
series = {Lecture Notes in Computer Science},
pages = {225246},
note = {To appear} } 
[inbook] bibtexD. Helms, G. Ehmen, und W. Nebel, "Analysis and Modeling of Subthreshold Leakage of RT Components under PTV and State Variation, von und (HS), C. O. U. O. O., Ed., pp. 2935.
@INBOOK{Helms07, chapter = {4},
pages = {2935},
title = {Analysis and Modeling of Subthreshold Leakage of RT Components under PTV and State Variation},
publisher = {BISVerlag der Carl von Ossietzky Universit{\"a}t Oldenburg},
year = {2007},
editor = {Carl von Ossietzky Universit{\"a}t Oldenburg und OFFIS (HS)},
author = {Domenik Helms and G{\"u}nter Ehmen and Wolfgang Nebel},
volume = {2},
series = {Selected Readings on Embedded HW/SWSystems},
month = {June},
booktitle = {Selected readings on embedded HW/SWsystems  ISSN 1860238X } } 
[inproceedings] bibtexS.~Kupferschmid, K.~Dräger, J.~Hoffmann, B.~Finkbeiner, H.~Dierks, A.~Podelski, und G.~Behrmann, "Uppaal/DMC  Abstractionbased Heuristics for Directed Model Checking.
@INPROCEEDINGS{KDHetal07,
author = {S.~Kupferschmid and K.~Dr{\"a}ger and J.~Hoffmann and B.~Finkbeiner and H.~Dierks and A.~Podelski and G.~Behrmann},
title = {Uppaal/DMC  Abstractionbased Heuristics for Directed Model Checking},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
year = {2007},
series = {Lecture Notes in Computer Science},
publisher = {SpringerVerlag} } 
[article] bibtexJ. Pang, W. Fokkink, R. Hofman, und R. Veldema, "Model checking a cache coherence protocol of a Java DSM implementation, pp. 143
@ARTICLE{PFHV07,
author = {Jun Pang and Wan Fokkink and Rutger Hofman and Ronald Veldema},
title = {Model checking a cache coherence protocol of a {J}ava {DSM} implementation},
journal = {Journal of Logic and Algebraic Programming},
year = {2007},
volume = {71},
pages = {143},
number = {1} } 
[inproceedings] bibtexT. Toben, "NonInterference Properties for DataType Reduction of Communicating Systems, pp. 619638.
@INPROCEEDINGS{Toben2007,
author = {Tobe Toben},
title = {NonInterference Properties for DataType Reduction of Communicating Systems},
booktitle = {Proceedings of the Sixth International Conference on Integrated Formal Methods (IFM 2007)},
year = {2007},
editor = {J. Davies and J. Gibbons},
volume = {4591},
series = {LNCS},
pages = {619638},
address = {Oxford, UK},
month = jul, publisher = {SpringerVerlag} } 
[proceedings] bibtexVerification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 1416, 2007, Proceedings.
@PROCEEDINGS{ProcVMCAI2007, title = {Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 1416, 2007, Proceedings},
year = {2007},
editor = {Byron Cook and Andreas Podelski},
volume = {4349},
series = {Lecture Notes in Computer Science},
publisher = {SpringerVerlag},
bibsource = {DBLP, http://dblp.unitrier.de},
booktitle = {VMCAI},
isbn = {3540697357} }
2006

[article] bibtexO. Åkerlund und others, "ISAAC, a framework for integrated safety analyses of functional, geometrical and human aspects
@ARTICLE{isaac06,
author = {Ove {\AA}kerlund and others},
title = {ISAAC, a framework for integrated safety analyses of functional, geometrical and human aspects},
journal = {ERTS},
year = {2006},
longauthor = {Ove {\AA}kerlund and Jakob Engblom and Bengt Werner and P. Bieber and C. Castel and L.Sagaspe and C. Seguin and E. B{\"o}de and A. L{\"u}dke and T. Peikenkamp and M. Bolzano and M. Bretschneider and M. Forte Da Cruz and M. Frisk and S. Metge and C. Papadopoulos and H. Trivedi and A. Cavallo and M. Cifaldi and J. Gauthier and A. Griffault and O. Lisagor and P. Person} } 
[inproceedings] bibtexO. Akerlund, P. Bieber, B. E., M. Bozzano, M. Bretschneider, C. Castel, A. Cavallo, M. Cifaldi, J. Gauthier, A. Griffault, O. Lisagor, A. Lüdtke, S. Metge, C. Papadopoulos, T. Peikenkamp, L. Sagaspe, C. Seguin, H. Trivedi, und L. Valacca, "ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects.
@INPROCEEDINGS{Akerlund_et_al2006,
author = {Akerlund, O. and Bieber, P. and Boede. E. and Bozzano, M. and Bretschneider, M. and Castel, C. and Cavallo, A. and Cifaldi, M. and Gauthier, J. and Griffault, A. and Lisagor, O. and L{\"u}dtke, A. and Metge, S. and Papadopoulos, C. and Peikenkamp, T. and Sagaspe, L. and Seguin, C. and Trivedi, H. and Valacca, L.},
title = {{ISAAC},
a framework for integrated safety analysis of functional, geometrical and human aspects},
booktitle = {Proceedings of the Embedded RealTime Software conference (ERTS'06).},
year = {2006},
owner = {luedtke},
timestamp = {2006.10.13} } 
[inproceedings] bibtex  Dokument aufrufenE. Böde, W. Damm, J. Hoyem, B. Josko, J. Niehaus, und M. Segelken, "Adding Value to Automotive Models, pp. 86102.
@INPROCEEDINGS{ASWSD_Damm_06:2006,
author = {Eckard B\"ode and Werner Damm and Jarl Hoyem and Bernhard Josko and J\"urgen Niehaus and Marc Segelken},
title = {Adding Value to Automotive Models},
booktitle = {Automotive Software  Connected Services in Mobile Networks},
year = {2006},
volume = {Volume 4147/2006},
series = {Lecture Notes in Computer Science},
pages = {86102},
organization = {ARTIST and NSF Workshop on Automotive Software Development},
publisher = {Springer Berlin / Heidelberg},
datemodified = {20061005 11:14:24 +0200},
url = {http://www.springerlink.com/content/yml61405270t10n6} } 
[article] bibtexB. Badban, J. van de Pol, O. Tveretina, und H. Zantema, "Generalizing DPLL and Satisfiability for Equalities
@ARTICLE{badban.bib,
author = {Bahareh Badban and Jaco van de Pol and Olga Tveretina and Hans Zantema},
title = {Generalizing DPLL and Satisfiability for Equalities},
year = {2006},
publisher = {Accepted for publication in the journal of Information and Computation I\&C} } 
[inproceedings] bibtex  Dokument aufrufenJ. Bauer, I. Schaefer, T. Toben, und B. Westphal, "Specification and Verification of Dynamic Communication Systems, pp. 189200.
@INPROCEEDINGS{BauerSchaeferTobenWestphal2006,
author = {Joerg Bauer and Ina Schaefer and Tobe Toben and Bernd Westphal},
title = {{S}pecification and {V}erification of {D}ynamic {C}ommunication {S}ystems},
booktitle = {Sixth International Conference on Application of Concurrency to System Design, 2006. ACSD 2006.},
year = {2006},
pages = {189200},
publisher = {IEEE Computer Society Press},
url = {http://seshome.informatik.unioldenburg.de/~berndw/2006_bauer_etal_acsd.pdf} } 
[inproceedings] bibtexR. Buschermöhle, H. Eekhoff, und B. Josko, "SUCCESS  Motivation, Vorgehensweise und Ergebnisse.
@INPROCEEDINGS{SUCCESS06,
author = {Ralf Buscherm{\"o}hle and Heike Eekhoff and Bernhard Josko},
title = {SUCCESS  Motivation, Vorgehensweise und Ergebnisse},
booktitle = {INFORMATIK 2006 Informatik f{\"u}r Menschen, Band 1, Beitr{\"a}ge der 36. Jahrestagung der Gesellschaft f{\"u}r Informatik e.V. (GI) 2.6.Oktober 2006 in Dresden.},
year = {2006},
publisher = {C. Hochberger, R{\"u}diger Liskowsky} } 
[inproceedings] bibtexT. Chothia, S. Orzan, J. Pang, und M. Torabi Dashti, "A framework for automatically checking anonymity with $\mu$CRL.
@INPROCEEDINGS{COPT06,
author = {Tom Chothia and Simona Orzan and Jun Pang and Mohammad {Torabi Dashti}},
title = {A framework for automatically checking anonymity with $\mu${CRL}},
booktitle = {Proc.\ 2nd Symposium on Trustworthy Global Computing},
year = {2006},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
note = {To appear} } 
[inproceedings] bibtexW. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, und B. Wirtz, "Automatic verification of hybrid systems with large discrete state space, pp. 276291.
@INPROCEEDINGS{DDHPP+06,
author = {Werner Damm and Stefan Disch and Hardi Hungar and Jun Pang and Florian Pigorsch and Christoph Scholl and Uwe Waldmann and Boris Wirtz},
title = {Automatic verification of hybrid systems with large discrete state space},
booktitle = {Proc.\ 4th Symposium on Automated Technology for Verification and Analysis},
year = {2006},
volume = {4218},
series = {Lecture Notes in Computer Science},
pages = {276291},
publisher = {Springer} } 
[inproceedings] bibtexY. Deng, J. Pang, und P. Wu, "Measuring anonymity with relative entropy.
@INPROCEEDINGS{DPW06,
author = {Yuxin Deng and Jun Pang and Peng Wu},
title = {Measuring anonymity with relative entropy},
booktitle = {Proc.\ 4th Workshop on Formal Aspects in Security and Trust},
year = {2006},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
note = {To appear} } 
[article] bibtexW. Fokkink und J. Pang, "Variations on ItaiRodeh leader election for anonymous rings and their analysis in PRISM, pp. 9811006
@ARTICLE{FokPan06,
author = {Wan Fokkink and Jun Pang},
title = {Variations on {I}tai{R}odeh leader election for anonymous rings and their analysis in {PRISM}},
journal = {Journal of Universal Computer Science},
year = {2006},
volume = {12},
pages = {9811006},
number = {8} } 
[inproceedings] bibtex  Dokument aufrufenD. Helms, G. Ehmen, und W. Nebel, "Analysis and Modeling of Subthreshold Leakage of RT Components under PTV and State Variation, pp. 220225.
@INPROCEEDINGS{Helms06,
author = {Domenik Helms and G{\"u}nter Ehmen and Wolfgang Nebel},
title = {Analysis and Modeling of Subthreshold Leakage of RT Components under PTV and State Variation},
booktitle = {Proceedings of the 2006 International Symposium on Low Power Electronics and Design},
year = {2006},
pages = {220225},
month = {October},
url = {http://ses.informatik.unioldenburg.de/download/bib/paper/Analysis and Modeling of Subthreshold Leakage of RTComponents under PTV and State Variation.pdf} } 
[inproceedings] bibtexD. Javaux, A. Lüdtke, P. Polson, F. Reuzeau, und N. Sarter, "Human Modeling and Complexity, pp. 242243.
@INPROCEEDINGS{Javaux_et_al2006,
author = {Javaux, D. and L{\"u}dtke, A. and Polson, P. and Reuzeau, F and Sarter, N.},
title = {Human Modeling and Complexity},
booktitle = {Proceedings of the International Conference on HumanComputer Interaction in Aeronautics (HCIAero 06)},
year = {2006},
editor = {F. Reuzeau and K. Corker and G. Boy},
pages = {242243},
address = {Toulouse, France},
publisher = {CépaduèsEditions},
note = {ISBN: 2.85428.748.7},
owner = {luedtke},
timestamp = {2006.10.13} } 
[techreport] bibtexB.~Josko und H. (Eds.), "Deliverable D3.2  Guidelines for establishing dependability requirements and performing hazard analysis, and for verification and validation of dependability requirements and constructing a safety case, Part 2  Formal Verification Techniques,".
@TECHREPORT{JD06,
author = {B.~Josko and H.~Dierks (Eds.)},
title = {Deliverable D3.2  Guidelines for establishing dependability requirements and performing hazard analysis, and for verification and validation of dependability requirements and constructing a safety case, Part 2  Formal Verification Techniques},
institution = {EASIS report},
year = {2006},
month = {November} } 
[inproceedings] bibtex  Dokument aufrufenJ. Klose, T. Toben, B. Westphal, und H. Wittke, "Check it out: On the Efficient Formal Verification of Life Sequence Charts.
@INPROCEEDINGS{2006_klose_etal_cav,
author = {Jochen Klose and Tobe Toben and Bernd Westphal and Hartmut Wittke},
title = {{C}heck it out: {O}n the {E}fficient {F}ormal {V}erification of {L}ife {S}equence {C}harts},
booktitle = {Proceedings of CAV 2006},
year = {2006},
editor = {Thomas Ball and Robert B. Jones},
volume = {4144},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
paes = {219233},
url = {http://seshome.informatik.unioldenburg.de/~berndw/2006_klose_etal_cav.pdf} } 
[inproceedings] bibtexS.~Kupferschmid, J.~Hoffmann, H.~Dierks, und G.~Behrmann, "Adapting an AI Planning Heuristic for Directed Model Checking.
@INPROCEEDINGS{KHDB06,
author = {S.~Kupferschmid and J.~Hoffmann and H.~Dierks and G.~Behrmann},
title = {Adapting an AI Planning Heuristic for Directed Model Checking},
booktitle = {13th International SPIN Workshop on Model Checking of Software},
year = {2006},
editor = {A.~Valmari},
volume = {3925},
series = {Lecture Notes in Computer Science},
address = {Vienna, Austria},
month = MAR, optpublisher = {SpringerVerlag} } 
[inproceedings] bibtexS. Leuchter, A. Lüdtke, und L. Urbas, "Human Performance Modellierung mit interoperablen kognitiven Agenten.
@INPROCEEDINGS{LeuchterLuedtkeUrbas2006,
author = {Leuchter, S and L{\"u}dtke, A. and Urbas, L.},
title = {Human Performance Modellierung mit interoperablen kognitiven Agenten},
booktitle = {48. Fachausschusssitzung Anthropotechnik der Deutschen Gesellschaft für Luft und Raumfahrt e.V., Cognitive Systems Engineering in der Fahrzeug und Prozessführung, 24.25. Oktober 2006, FraunhoferIITB, Karlsruhe.},
year = {2006},
note = {(to be published)},
owner = {luedtke},
timestamp = {2006.10.13} } 
[inproceedings] bibtexO. Lisagor, M. Pretzer, C. Seguin, D. J. Pumfrey, F. Iwu, und T. Peikenkamp, "Towards Safety Analysis of Highly Integrated Technologically Heterogeneous Systems  A DomainBased Approach for Modelling System Failure Logic.
@INPROCEEDINGS{issc06,
author = {O. Lisagor and M. Pretzer and C. Seguin and D. J. Pumfrey and F. Iwu and T. Peikenkamp},
title = {Towards Safety Analysis of Highly Integrated Technologically Heterogeneous Systems  A DomainBased Approach for Modelling System Failure Logic},
booktitle = {Proceedings of the 24th International System Safety Conference (ISSC)},
year = {2006},
address = {Albuquerque, New Mexico, USA} } 
[article] bibtexA. Lüdtke, "Prognose potentieller Bedienungsfehler beim Entwurf Sicherheitskritischer Systeme, p. 4
@ARTICLE{Luedtke2006,
author = {L{\"u}dtke, A.},
title = {Prognose potentieller Bedienungsfehler beim Entwurf Sicherheitskritischer Systeme},
journal = {it Information Technology},
year = {2006},
volume = {6},
pages = {4 Seiten},
month = {August},
owner = {luedtke},
timestamp = {2006.10.13} } 
[inproceedings] bibtexA. Lüdtke, A. Cavallo, L. Christophe, M. Cifaldi, M. Fabbri, und D. Javaux, "Human Error Analysis based on a Cognitive Architecture, pp. 4047.
@INPROCEEDINGS{Luedtke_et_al2006,
author = {L{\"u}dtke, A. and Cavallo, A. and Christophe, L. and Cifaldi, M. and Fabbri, M. and Javaux, D},
title = {Human Error Analysis based on a Cognitive Architecture},
booktitle = {Proceedings of the International Conference on HumanComputer Interaction in Aeronautics (HCIAero 06)},
year = {2006},
editor = {F. Reuzeau and K. Corker and G. Boy},
pages = {4047},
address = {Toulouse, France},
publisher = {CépaduèsEditions},
note = {ISBN: 2.85428.748.7},
owner = {luedtke},
timestamp = {2006.05.28} } 
[inproceedings] bibtexA. Lüdtke und L. Weber, "Human Error Analysis Tool, pp. 252253.
@INPROCEEDINGS{LuedtkeWeber2006,
author = {L{\"u}dtke, A. and Weber, L.},
title = {Human Error Analysis Tool},
booktitle = {Proceedings of the International Conference on HumanComputer Interaction in Aeronautics (HCIAero 06)},
year = {2006},
editor = {F. Reuzeau and K. Corker and G. Boy},
pages = {252253},
address = {Toulouse, France},
publisher = {CépaduèsEditions},
note = {ISBN: 2.85428.748.7},
owner = {luedtke},
timestamp = {2006.09.02} } 
[inproceedings] bibtexT. Toben und B. Westphal, "On the Expressive Power of Life Sequence Charts, pp. 3343.
@INPROCEEDINGS{TobenWestphal2006b,
author = {Tobe Toben and Bernd Westphal},
title = {{O}n the {E}xpressive {P}ower of {L}ife {S}equence {C}harts},
booktitle = {Proceedings of the 32nd Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'06)},
year = {2006},
editor = {Ji\v{r}\'{i} Wiedermann and Gerard Tel and Jaroslav Pokorn\'{y} and M\'{a}ria Bielikov\'{a} and J\'{u}lius \v{S}tuller},
volume = {2},
pages = {3343},
address = {M\v{e}\v{r}\'{i}n, Czech Republic},
month = jan, publisher = {Institute of Computer Science AS CR, Prague} } 
[inproceedings] bibtex  Dokument aufrufenB. Westphal und T. Toben, "The Good, the Bad and the Ugly: Wellformdness of Life Sequence Charts, pp. 230246.
@INPROCEEDINGS{2006_westphal_toben_fase,
author = {Bernd Westphal and Tobe Toben},
title = {{T}he {G}ood, the {B}ad and the {U}gly: {W}ellformdness of {L}ife {S}equence {C}harts},
booktitle = {Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE 2006)},
year = {2006},
editor = {Luciano Baresi and R. Heckel},
volume = {3922},
series = {Lecture Notes in Computer Science},
pages = {230246},
address = {Vienna, Austria},
month = mar, publisher = {Springer},
url = {http://seshome.informatik.unioldenburg.de/~berndw/2006_westphal_toben_fase.pdf} }
2005

[incollection] bibtexE. Brinksma, G. Coulson, I. Crnkovic, A. Evans, S. Gérard, S. Graf, H. Hermanns, J. M. Jézeqél, B. Jonsson, N. Plouzeau, A. Ravn, P. Schnoebelen, F. Terrier, und A. Votintseva, "Part II: ComponentBased Design and Integration Platforms, Bouyssounouse, B. und Sifakis, J., Eds., pp. 103214.
@INCOLLECTION{BrinksmaEtAl:05,
author = {E. Brinksma and G. Coulson and I. Crnkovic and A. Evans and S. G\'{e}rard and S. Graf and H. Hermanns and J.M. J\'{e}zeq\'{e}l and B. Jonsson and N. Plouzeau and A. Ravn and Ph. Schnoebelen and F. Terrier and A. Votintseva},
title = {Part II: ComponentBased Design and Integration Platforms},
booktitle = {Embedded Systems Design: The {ARTIST} Roadmap for Research and Development},
publisher = {Springer},
year = {2005},
editor = {B. Bouyssounouse and J. Sifakis},
number = {3436},
series = {LNCS},
pages = {103214},
note = {available at http://www.artistembedded.org/Roadmaps/index.html} } 
[article] bibtexW. Damm, B. Josko, A. Pnueli, und A. Votintseva, "A DiscreteTime UML Semantics for Concurrency and Communication in SafetyCritical Applications, pp. 81115
@ARTICLE{DammJoskoPnueliVotintseva2005,
author = {Werner Damm and Bernhard Josko and Amir Pnueli and Angelika Votintseva},
title = {A DiscreteTime UML Semantics for Concurrency and Communication in SafetyCritical Applications},
journal = {Science of Computer Programming},
year = {2005},
volume = {55},
pages = {81115},
number = {13},
month = {March},
note = {available at http://authors.elsevier.com/sd/article/S0167642304001479} } 
[inproceedings] bibtexW. Damm, G. Pinto, und S. Ratschan, "Guaranteed Termination in the Verification of LTL Properties of Nonlinear Robust Hybrid Systems.
@INPROCEEDINGS{damm2005guaranteed,
author = {Werner Damm and Guilherme Pinto and Stefan Ratschan},
title = {Guaranteed Termination in the Verification of {LTL} Properties of Nonlinear Robust Hybrid Systems},
year = {2005},
note = {Submitted for Publication, 13 pages},
abstract = {We present a novel approach to the automatic verification of LTL requirements of nonlinear discretetime hybrid systems. The verification tool uses an intervalbased constraint solver for nonlinear robust constraints to compute incrementally refined abstractions. Although the problem is undecidable, we prove termination of abstraction refinement based verification of such properties for the class of robust nonlinear hybrid systems, thus significantly extending previous semidecidability results. We argue, that safety critical control applications are robust hybrid systems. We give first results on the application of this approach to a variant of an aircraft collision avoidance protocol.},
pdf = {damm2005guaranteed.pdf},
postscript = {damm2005guaranteed.ps} } 
[article] bibtexW. Damm und B. Westphal, "Live and Let Die: LSCbased Verification of UMLModels, pp. 117159
@ARTICLE{DammWestphal2005,
author = {Werner Damm and Bernd Westphal},
title = {Live and Let Die: {LSC}based Verification of {UML}Models},
journal = {Science of Computer Programming},
year = {2005},
volume = {55},
pages = {117159},
number = {13},
month = mar } 
[techreport] bibtexH.~Dierks, "Heuristic Guided ModelChecking of RealTime Systems,".
@TECHREPORT{Die05,
author = {H.~Dierks},
title = {{Heuristic Guided ModelChecking of RealTime Systems}},
institution = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
year = {2005},
note = {full version} } 
[inproceedings] bibtexH.~Dierks, "Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA.
@INPROCEEDINGS{Die05b,
author = {H.~Dierks},
title = {{Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA}},
booktitle = {{Proceedings of the ICAPS'05 Workshop on Verification and Validation of ModelBased Planning and Scheduling Systems}},
year = {2005} } 
[unpublished] bibtexTime, Abstraction and Heuristics  Automatic Verification and Planning of Timed Systems using Abstraction and Heuristics.
@UNPUBLISHED{Die05Hab,
author = {H.~Dierks},
title = {{Time, Abstraction and Heuristics  Automatic Verification and Planning of Timed Systems using Abstraction and Heuristics}},
note = {Habilitation thesis},
month = JUL, year = {2005},
http = {Dierks2005Habil.pdf} } 
[incollection] bibtexA. Lüdtke, "Kognitive Analyse Formaler Sicherheitskritischer Steuerungssysteme auf Basis eines integrierten MenschMaschineModells, et al., W. D., Ed.
@INCOLLECTION{Luedtke2005a,
author = {L{\"u}dtke, A.},
title = {{Kognitive Analyse Formaler Sicherheitskritischer Steuerungssysteme auf Basis eines integrierten MenschMaschineModells}},
booktitle = {{Ausgezeichnete Informatikdissertationen 2004, Gesellschaft f{\"u}r Informatik e.V.}},
publisher = {{K{\"o}llen Druck und Verlag GmbH}},
year = {2005},
editor = {D. Wagner et al.},
series = {Lecture Notes in Informatics (LNI)},
address = {Bonn},
edition = {{GIEdition}},
note = {ISBN: 3885794098} } 
[incollection] bibtexA. Lüdtke, "Kognitive Analyse Formaler Sicherheitskritischer Steuerungssysteme auf Basis eines integrierten MenschMaschineModells.
@INCOLLECTION{Luedtke2005,
author = {L{\"u}dtke, A.},
title = {{Kognitive Analyse Formaler Sicherheitskritischer Steuerungssysteme auf Basis eines integrierten MenschMaschineModells}},
booktitle = {{Dissertationen zur K{\"u}nstlichen Intelligenz, DISKI}},
publisher = {{Akad. Verl.Ges. Aka}},
year = {2005},
volume = {288},
address = {Berlin},
note = {ISBN 3898382885} } 
[inproceedings] bibtexA. Lüdtke und S. Leuchter, "Human Error Analyse auf Basis Zweckbestimmter Kognitiver Modelle.
@INPROCEEDINGS{LuedtkeLeuchter2005,
author = {L{\"u}dtke, A. and Leuchter, S.},
title = {{Human Error Analyse auf Basis Zweckbestimmter Kognitiver Modelle}},
booktitle = {{WorkshopProceedings der 5. fach{\"u}bergreifenden Konferenz Mensch und Computer, 4.7. August 2005, Linz, {\"O}sterreich}},
year = {2005},
editor = {A. Auinger},
publisher = {{\"O}sterreichische Computer Gesellschaft},
howpublished = {{Angenommen zum Workshop Interaktion bei Prozess und Fahrzeugf{\"u}hrung im Rahmen der Tagung Mensch \& Computer}} } 
[inproceedings] bibtexA. Lüdtke und C. Möbus, "A Case Study for Using a Cognitive Model of Learned Carelessness in Cognitive Engineering.
@INPROCEEDINGS{LuedtkeMoebus2005,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{A Case Study for Using a Cognitive Model of Learned Carelessness in Cognitive Engineering}},
booktitle = {{Proceedings of HCI International'05 the 11th International Conference on HumanComputer Interaction}},
year = {2005},
editor = {G. Salvendy},
address = {Mahwah, New Jersey},
publisher = {Lawrence Erlbaum Associates, Inc.},
note = {ISBN 0805858075, CDROM} } 
[inproceedings] bibtexC. Mrugalla, O. Robbe, I. Schinz, T. Toben, und B. Westphal, "Formal Verification of a Sensor Voting and Monitoring UML Model.
@INPROCEEDINGS{MrugallaRobbeSchinzTobenWestphal2005,
author = {Christian Mrugalla and Oliver Robbe and Ingo Schinz and Tobe Toben and Bernd Westphal},
title = {Formal Verification of a Sensor Voting and Monitoring UML Model},
booktitle = {Proceedings of the 4th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML 2005)},
year = {2005},
editor = {Siv Hilde Houmb, Jan J\"{u}rjens, Robert France},
month = sep, publisher = {Technische Universit\"{a}t M\"{u}nchen} } 
[incollection] bibtexC. Möbus, O. Schröder, und A. Lüdtke, "Trainingseinheit 7: Entscheiden unter Unsicherheit., Franke, G. und Selka, R., Eds.
@INCOLLECTION{MoebusSchroederLuedtke2005,
author = {M{\"o}bus, C. and Schr{\"o}der, O. and L{\"u}dtke, A.},
title = {{Trainingseinheit 7: Entscheiden unter Unsicherheit.}},
booktitle = {{Entwicklung und Förderung der strategischen Handlungsflexibilität, Band 3: Analysieren  Modellieren  Entscheiden}},
publisher = {W.BertelsmannVerlag},
year = {2005},
editor = {G. Franke and R. Selka},
address = {Bielefeld},
note = {ISBN 3763906541},
owner = {luedtke},
timestamp = {2006.10.13} } 
[incollection] bibtexC. Möbus, O. Schröder, und A. Lüdtke, "Entscheidung unter Unsicherheit, G. Franke, S. R., Ed., pp. 4969.
@INCOLLECTION{MoebusSchroederLuedtke2005a,
author = {M{\"o}bus, C. and Schr{\"o}der, O. and L{\"u}dtke, A.},
title = {{Entscheidung unter Unsicherheit}},
booktitle = {{Entwicklung und F{\"o}rderung der strategischen Handlungsflexibilit{\"a}t, Band 3: Analysieren  Modellieren  Entscheiden}},
publisher = {W.BertelsmannVerlag},
year = {2005},
editor = {G. Franke, R. Selka},
pages = {4969},
address = {Bielefeld},
note = {ISBN 3763906541} } 
[inproceedings] bibtexH. Seebold, A. Lüdtke, und C. Möbus, "Bayesian Belief Network based Diagnostics in a Problemoriented Learning Environment for Cardiology.
@INPROCEEDINGS{SeeboldLuedtkeMoebus2005,
author = {Seebold, H and L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{Bayesian Belief Network based Diagnostics in a Problemoriented Learning Environment for Cardiology}},
booktitle = {{Proceedings of Training, Education \& Simulation International 2005 (TESI 2005), 22.24. March 2005, Maastricht, The Netherlands}},
year = {2005},
owner = {luedtke},
timestamp = {2006.10.13} } 
[inproceedings] bibtexB. Westphal, "LSC Verification for UML Models with Unbounded Creation and Destruction, pp. 133145.
@INPROCEEDINGS{Westphal2005,
author = {Bernd Westphal},
title = {{LSC} Verification for UML Models with Unbounded Creation and Destruction},
booktitle = {Proceedings of the Workshop on Software Model Checking (SoftMC 2005)},
year = {2005},
editor = {Byron Cook, Scott Stoller, Willem Visser},
volume = {144},
number = {3},
series = {ENTCS},
pages = {133145},
month = jul, publisher = {Elsevier B.V.},
xpardate = {Mon Aug 8 14:53:37 MEST 2005},
xtopics = {umlverif uml ruve} } 
[mastersthesis] bibtexG. Ehmen, "Datenabhängige RTEbenenModellierung von Leckströmen in tiefen SubMikrometerCMOSTechnologien,".
@MASTERSTHESIS{diplom05,
author = {Ehmen, G{\"u}nter},
title = {Datenabh{\"a}ngige RTEbenenModellierung von Leckstr{\"o}men in tiefen SubMikrometerCMOSTechnologien},
school = {Oldenburg, Univ},
year = {2005},
comment = {Nebel, Wolfgang H. [Gutachter] ; Helms, Domenik [Gutachter]},
owner = {guenter},
timestamp = {11.58.2008} }
2004

[incollection] bibtexW. Damm und B. Westphal, "Introduction to Subject Area Charts, pp. 322324.
@INCOLLECTION{DammWestphal2004a,
author = {Werner Damm and Bernd Westphal},
title = {Introduction to Subject Area Charts},
year = {2004},
pages = {322324},
crossref = {Ehrig2004},
xpardate = {Thu May 19 09:32:33 MEST 2005},
xtopics = {use lsc} } 
[inproceedings] bibtexB. Becker, M. Behle, F. Eisenbrand, M. Fränzle, M. Herbstritt, C. Herde, J. Hoffmann, D. Kröning, B. Nebel, I. Polian, und R. Wimmer, "Bounded Model Checking and Inductive Verification of Hybrid Discretecontinuous Systems, pp. 6575.
@INPROCEEDINGS{berbec:2004,
author = {Bernd Becker and Markus Behle and Fritz Eisenbrand and Martin Fr\"anzle and Marc Herbstritt and Christian Herde and Joerg Hoffmann and Daniel Kr\"oning and Bernhard Nebel and Ilia Polian and Ralf Wimmer},
title = {{Bounded Model Checking and Inductive Verification of Hybrid Discretecontinuous Systems}},
booktitle = {ITG/GI/GMMWorkshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen''},
year = {2004},
pages = {6575},
iranote = {AVACS H2},
isbn = {3832224866},
language = {USenglish},
public = {no},
timestamp = {1080559316} } 
[incollection] bibtexM. Brill, R. Buschermöhle, W. Damm, J. Klose, B. Westphal, und H. Wittke, "Formal Verification of LSC's in the Development Process, Ehrig, H., Damm, W., , M. G., Reif, W., Schnieder, E., und Westkämper, E., Eds.
@INCOLLECTION{BrDaKlWeWi:04,
author = {Matthias Brill and Ralf Buscherm\"{o}hle and Werner Damm and Jochen Klose and Bernd Westphal and Hartmut Wittke},
title = {Formal Verification of {LSC}'s in the Development Process},
booktitle = {Integration of Software Specification Techniques for Applications in Engineering},
year = {2004},
editor = {Hartmut Ehrig and Werner Damm and Martin Gro\s{}eRhode and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk\"{a}mper},
number = {3147},
series = {LNCS},
note = {(C) SpringerVerlag 2004, may not be further reproduced without their permission, and is published in Volume 3147 of the LNCS series.},
pdf = {spplncsuseverif.pdf} } 
[incollection] bibtexM. Brill, W. Damm, J. Klose, B. Westphal, und H. Wittke, "Live Sequence Charts, Ehrig, H., Damm, W., , M. G., Reif, W., Schnieder, E., und Westkämper, E., Eds.
@INCOLLECTION{BrillDammKlose2004,
author = {Matthias Brill and Werner Damm and Jochen Klose and Bernd Westphal and Hartmut Wittke},
title = {Live Sequence Charts},
booktitle = {Integration of Software Specification Techniques for Applications in Engineering},
year = {2004},
editor = {Hartmut Ehrig and Werner Damm and Martin Gro\s{}eRhode and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk\"{a}mper},
number = {3147},
series = {LNCS},
note = {(C) SpringerVerlag 2004, may not be further reproduced without their permission, and is published in Volume 3147 of the LNCS series.},
pdf = {spplncsusecharts.pdf} } 
[inproceedings] bibtexJ. Y. Brunel, W. Damm, A. Ferrari, U. Freund, B. Josko, S. Kowalewski, A. SangiovanniVincentelli, M. Torngren, T. Thurner, und H. von Hasseln, "The Future Design Scenario and The SEA Inititative.
@INPROCEEDINGS{vonHasselnEtal2004,
author = {J.Y. Brunel and W. Damm and A. Ferrari and U. Freund and B. Josko and S. Kowalewski and A. SangiovanniVincentelli and M. Torngren and T. Thurner and H. von Hasseln},
title = {The Future Design Scenario and The {SEA} Inititative},
booktitle = {{IFAC} Symposium on Advances in Automotive Control},
year = {2004},
address = {University of Salerno, Italy},
pdf = {FutureDesignScenario.pdf} } 
[article] bibtexR. Buschermöhle, M. Brörkens, I. Brückner, W. Damm, W. Hasselbring, B. Josko, C. Schulte, und T. Wolf, "Model Checking  Grundlagen und Praxiserfahrungen
@ARTICLE{bbbdhjsw:2003,
author = {Buscherm{\"o}hle, R. and Br{\"o}rkens, M. and Br{\"u}ckner, I. and Damm, W. and Hasselbring, W. and Josko, B. and Schulte, C. and Wolf, T.},
title = {{M}odel {C}hecking  {G}rundlagen und {P}raxiserfahrungen},
journal = {{I}nformatik {S}pektrum},
year = {2004},
number = {2},
month = {april},
note = {to appear},
abstract = { },
pdf = {MCP.pdf} } 
[inproceedings] bibtexW. Damm, H. Hungar, und E. R. Olderog, "On the Verification of Cooperating Traffic Agents, pp. 77110.
@INPROCEEDINGS{DHO04,
author = {W. Damm and H. Hungar and E.R. Olderog},
title = {On the Verification of Cooperating Traffic Agents},
booktitle = {Proc.\ FMCO '03: Formal Methods for Components and Objects},
year = {2004},
editor = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.P. de Roever},
series = {LNCS 3188},
pages = {77110},
abstract = {This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind "a collision will never occur", and whose premises can either be established by offline analysis of the worstcase behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. In a companion paper we will show, how such local proof obligations can be discharged automatically. },
key = {DHO04} } 
[inproceedings] bibtexH.~Dierks, "Heuristic Guided ModelChecking of RealTime Systems (Extended Abstract), pp. 1416.
@INPROCEEDINGS{Die04b,
author = {H.~Dierks},
title = {{Heuristic Guided ModelChecking of RealTime Systems (Extended Abstract)}},
booktitle = {{Proceedings of the 16th Nordic Workshop on Programming Theory}},
year = {2004},
editor = {P.~Pettersson and Wang Yi},
series = {Technical Report 2004041},
pages = {1416},
month = OCT, organization = {Uppsala University, Sweden},
issn = {14043203} } 
[article] bibtexH.~Dierks, "Comparing ModelChecking and Logical Reasoning for RealTime Systems, pp. 104120
@ARTICLE{Die04,
author = {H.~Dierks},
title = {{Comparing ModelChecking and Logical Reasoning for RealTime Systems}},
journal = {Formal Aspects of Computing},
year = {2004},
volume = {16},
pages = {104120},
number = {2},
month = MAY, optnote = {to appear} } 
[conference] bibtexA. Lüdtke und C. Möbus, "Automatisierte Prognose von Bedienungsfehlern bei der Entwicklung von Pilotenassistenzsystemen, pp. 241270.
@CONFERENCE{LuedtkeMoebus2004a,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{Automatisierte Prognose von Bedienungsfehlern bei der Entwicklung von Pilotenassistenzsystemen}},
booktitle = {{Verl{\"a}sslichkeit der MenschMaschineInteraktion: 46. Fachausschusssitzung Anthropotechnik der Deutschen Gesellschaft f{\"u}r Luft und Raumfahrt e.V.}},
year = {2004},
editor = {M. Grandt},
number = {200403},
series = {DGLRBericht},
pages = {241270},
address = {Bonn},
publisher = {{Deutsche Gesellschaft f{\"u}r Luft und Raumfahrt e.V.}},
note = {ISBN 3932182367} } 
[inproceedings] bibtexA. Lüdtke und C. Möbus, "A Cognitive Pilot Model to Predict Learned Carelessness for System Design.
@INPROCEEDINGS{LuedtkeMoebus2004b,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {A Cognitive Pilot Model to Predict Learned Carelessness for System Design},
booktitle = {{Proceedings of HCIAero the International Conference on HumanComputer Interaction in Aeronautics}},
year = {2004},
editor = {A. Pritchett and A. Jackson},
address = {Toulouse, France},
month = {September 29  October 1},
note = {CDROM} } 
[incollection] bibtexA. Lüdtke und C. Möbus, "Überprüfung eines Lernenden Pilotenmodells durch Rekonstruktion von Handlungsprotokollen, Steffens, C., Thüring, M., und Urbas, L., Eds., pp. 160180.
@INCOLLECTION{LuedtkeMoebus2004,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{{\"U}berpr{\"u}fung eines Lernenden Pilotenmodells durch Rekonstruktion von Handlungsprotokollen}},
booktitle = {{Entwerfen und Gestalten: 5. Berliner Werkstatt MenschMaschineSysteme 2003}},
publisher = {VDI Verlag GmbH},
year = {2004},
editor = {C. Steffens and M. Th{\"u}ring and L. Urbas},
pages = {160180},
address = {D{\"u}sseldorf},
note = {ISBN 3183016222} } 
[inproceedings] bibtexA. Metzner, "Why Model Checking Can Improve WCET Analysis.
@INPROCEEDINGS{metzner04,
author = {Alexander Metzner},
title = {{Why Model Checking Can Improve WCET Analysis}},
booktitle = {Proceeding of the $16^{th}$ Internation Conference on Computer Aided Verification (CAV'04)},
year = {2004},
volume = {3114},
series = {Lecture Notes in Computer Science} } 
[inproceedings] bibtexT. Peikenkamp, E. Böde, I. Brückner, H. Spenke, M. Bretschneider, und H.J., "Modelbased Safety Analysis of a Flap Control System.
@INPROCEEDINGS{incose2004,
author = {T. Peikenkamp and E. B{\"o}de and I. Br{\"u}ckner and H. Spenke and M. Bretschneider and {H.J.} Holberg},
title = {Modelbased {S}afety {A}nalysis of a {F}lap {C}ontrol {S}ystem},
booktitle = {Proceedings of the INCOSE 2004  14th Annual International Symposium},
year = {2004},
address = {Toulouse},
pdf = {incose2004.pdf} } 
[inproceedings] bibtexI. Schinz, T. Toben, C. Mrugalla, und B. Westphal, "The Rhapsody UML Verification Environment.
@INPROCEEDINGS{SchinzTobenMrugallaWestphal2004,
author = {Ingo Schinz and Tobe Toben and Christian Mrugalla and Bernd Westphal},
title = {{T}he {R}hapsody {UML} {V}erification {E}nvironment},
booktitle = {Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004)},
year = {2004},
editor = {Jorge R. Cuellar and Zhiming Liu},
address = {Beijing, China},
month = {sep},
publisher = {IEEE},
postscript = {schinz_i_rhapumlverif.ps.gz} } 
[inproceedings] bibtexH. Seebold, A. Lüdtke, und C. Möbus, "The Engineering and Evaluation of an Intelligent ProblemOriented Learning Environment.
@INPROCEEDINGS{SeeboldLuedtkeMoebus2004,
author = {Seebold, H and L{\"u}dtke, A. and M{\"o}bus, C.},
title = {The Engineering and Evaluation of an Intelligent ProblemOriented Learning Environment.},
booktitle = {{Proceedings of the Workshop on Teaching and Learning Systems, The Role of Artificial Intelligence in Past, Present and Future, 15th Meeting of the GI Special Interest Group Intelligent Teaching and Learning Systems, KI 2004.}},
year = {2004},
editor = {Martens, A. and Harrer, A.},
owner = {luedtke},
timestamp = {2006.10.13} } 
[book] bibtexIntegration of Software Specification Techniques for Applications in Engineering, Ehrig, H., Damm, W., Desel, J., GroßeRhode, M., Reif, W., Schnieder, E., und Westkämper, E., Eds.
@BOOK{Ehrig2004, title = {Integration of Software Specification Techniques for Applications in Engineering},
publisher = {SpringerVerlag},
year = {2004},
editor = {Hartmut Ehrig and Werner Damm and J\"{o}rg Desel and Martin Gro{\ss}eRhode and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk\"{a}mper},
number = {3147},
series = {Lecture Notes in Computer Science} }
2003

[inproceedings] bibtexH.~Dierks und J.~Tapken, "Moby/DC  A Tool for ModelChecking Parametric RealTime Specifications, pp. 271277.
@INPROCEEDINGS{DT03,
author = {H.~Dierks and J.~Tapken},
title = {{Moby/DC  A Tool for ModelChecking Parametric RealTime Specifications}},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
year = {2003},
volume = {2619},
series = {Lecture Notes in Computer Science},
pages = {271277},
publisher = {SpringerVerlag},
crossref = {LNCS2619} } 
[phdthesis] bibtexT. Bienmüller, "Reducing Complexity for the Verification of Statemate Designs,".
@PHDTHESIS{Bienmueller:2003,
author = {Tom Bienm{\"u}ller},
title = {Reducing {C}omplexity for the {V}erification of {S}tatemate {D}esigns},
school = {Carl von Ossietzky Universit\"at Oldenburg Germany},
year = {2003},
month = jun, note = {ISSN 09462910} } 
[inproceedings] bibtexM. Bozzano, Villafiorita, O. A. Akerlund, P. Bieber, C. Bougnol, B. E., M. Bretschneider, A. Cavallo, C. Castel, M. Cifaldi, A. Cimatti, A. Griffault, C. Kehren, B. Lawrence, A. Lüdtke, S. Metge, C. Papadopoulos, R. Passatello, T. Peikenkamp, P. Persson, C. Seguin, L. Trotta, L. Valacca, und G. Zacco, "ESACS: an Integrated Methodology for Design and Safety Analysis of Complex Systems.
@INPROCEEDINGS{Bozzano_et_al2003,
author = {Bozzano, M. and Villafiorita and A. Akerlund, O. and Bieber, P. and Bougnol, C. and Boede. E. and Bretschneider, M. and Cavallo, A. and Castel, C. and Cifaldi, M. and Cimatti, A. and Griffault, A. and Kehren, C. and Lawrence, B. and L{\"u}dtke, A. and Metge, S. and Papadopoulos, C. and Passatello, R. and Peikenkamp, T. and Persson, P. and Seguin, C. and Trotta, L. and Valacca, L. and Zacco, G.},
title = {{ESACS: an Integrated Methodology for Design and Safety Analysis of Complex Systems}},
booktitle = {{European Safety and Reliability Conference (ESREL), June 15  18, 2003, Maastricht, The Netherlands}},
year = {2003},
owner = {luedtke},
timestamp = {2006.12.13} } 
[inproceedings] bibtexW. Damm, B. Josko, A. Pnueli, und A. Votintseva, "Understanding UML: A Formal Semantics of Concurrency and Communication in RealTime UML.
@INPROCEEDINGS{DammJoskoPnueliVotintseva2003,
author = {W. Damm and B. Josko and A. Pnueli and A. Votintseva},
title = {{U}nderstanding {UML}: {A} {F}ormal {S}emantics of {C}oncurrency and {C}ommunication in {R}eal{T}ime {UML}},
booktitle = {Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO)},
year = {2003},
series = {LNCS},
publisher = {SpringerVerlag} } 
[article] bibtexW. Damm, C. Schulte, M. Segelken, H. Wittke, U. Higgen, und M. Eckrich, "Formale Verifikation von ASCET Modellen im Rahmen der Entwicklung der Aktivlenkung, pp. 340345
@ARTICLE{ascet_afs_verif:2003,
author = {W. Damm and C. Schulte and M. Segelken and H. Wittke and U. Higgen and M. Eckrich},
title = {{F}ormale {V}erifikation von {ASCET} {M}odellen im {R}ahmen der {E}ntwicklung der {A}ktivlenkung},
journal = {{L}ecture {N}otes in {I}nformatics},
year = {2003},
volume = {P34},
pages = {340345},
month = {May},
isbn = {3885793636},
pdf = {Aktivlenkung_ASCET_verif.pdf} } 
[inproceedings] bibtexW. Damm und B. Westphal, "Live and Let Die: LSCbased Verification of UMLModels.
@INPROCEEDINGS{DW03,
author = {W. Damm and B. Westphal},
title = {Live and {L}et {D}ie: {LSC}based {V}erification of {UML}{M}odels},
booktitle = {Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO)},
year = {2003},
series = {LNCS},
publisher = {SpringerVerlag} } 
[article] bibtexH.~Dierks und E.R.~Olderog, "Temporale Spezifikationslogiken, p. a1a4
@ARTICLE{DO03,
author = {H.~Dierks and E.R.~Olderog},
title = {{Temporale Spezifikationslogiken}},
journal = {atAutomatisierungstechnik},
year = {2003},
volume = {51},
pages = {A1A4},
number = {2} } 
[conference] bibtexM. Fränzle und C. Herde, "Efficient SAT engines for concise logics: Accelerating proof search for zeroone linear constraint systems, pp. 302316.
@CONFERENCE{IMM200302531,
author = {M. Fr{\"a}nzle and C. Herde},
title = {Efficient {SAT} engines for concise logics: Accelerating proof search for zeroone linear constraint systems},
booktitle = {Logic for Programming, Artificial Intelligence and Reasoning ({LPAR} 2003)},
year = {2003},
editor = {Moshe Y. Vardi, Andrei Voronkov},
volume = {2850},
series = {{LNCS},
subseries {LNAI}},
pages = {302316},
month = {sep},
publisher = {Springer Verlag},
abstract = {We investigate the problem of generalizing acceleration techniques as found in recent satisfiability engines for conjunctive normal forms (CNFs) to linear constraint systems over the Booleans. The rationale behind this research is that rewriting the propositional formulae occurring in e.g. bounded model checking ({BMC}) [Biere, Cimatti,Zhu, 1999] to {CNF} requires a blowup in either the formula size (worstcase exponential) or in the number of propositional variables (linear, thus yielding a worstcase exponential blowup of the search space). We demonstrate that acceleration techniques like observation lists and lazy clause evaluation [Moskewicz e.a., 2001] as well as the more traditional nonchronological backtracking and learning techniques generalize smoothly to DavisPutnamlike resolution procedures for the very concise propositional logic of linear constraint systems over the Booleans. Despite the more expressive input language, the performance of our prototype implementation comes surprisingly close to that of stateoftheart {CNFSAT} engines like ZChaff [Moskewicz e.a., 2001]. First experiments with bounded modelconstruction problems show that the overhead in the satisfiability engine that can be attributed to the richer input language is often amortized by the conciseness gained in the propositional encoding of the {BMC} problem.},
keywords = {Satisfiability; nonclausal propositional logic; zeroone linear constraint systems; proof search; acceleration techniques},
postscript = {LPAR03_Fraenzle_Herde.ps} } 
[article] bibtexM. Fränzle, J. Niehaus, A. Metzner, und W. Damm, "A Semantics for Distributed Execution of STATEMATE, pp. 390405
@ARTICLE{distributedstatemate,
author = {Martin Fr{\"a}nzle and J{\"u}rgen Niehaus and Alexander Metzner and Werner Damm},
title = {A Semantics for Distributed Execution of {STATEMATE}},
journal = {Formal Aspects of Computing},
year = {2003},
volume = {15},
pages = {390405},
number = {4},
month = {December},
note = {ISSN: 09345043},
publisher = {SpringerVerlag London Ltd} } 
[phdthesis] bibtexJ. Klose, "Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior,".
@PHDTHESIS{Klose2003,
author = {Jochen Klose},
title = {Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior},
school = {Carl von Ossietzky Universit\"{a}t Oldenburg},
year = {2003},
postscript = {diss_klose.ps.gz} } 
[inproceedings] bibtexJ. Klose und B. Westphal, "Verification of a Radiobased Signaling System Using Scenarios, pp. 4962.
@INPROCEEDINGS{KloseWestphal2002a,
author = {Jochen Klose and Bernd Westphal},
title = {Verification of a Radiobased Signaling System Using Scenarios},
booktitle = {International Workshop on Software Specification of Safety Relevant Transportation Control Tasks, 23  24 April 2002, Braunschweig},
year = {2003},
editor = {Eckehard Schnieder},
number = {535},
series = {FortschrittBerichte VDI, Reihe 12, Verkehrstechnik/Fahrzeugtechnik},
pages = {4962},
address = {D\"usseldorf},
publisher = {VDI Verlag},
abstract = {This paper presents a sequence chartbased design methodology for the formal verification of a system under design. Since standard Message Sequence Charts are neither expressive enough nor do they have a sufficient formal semantics we introduce Live Sequence Charts (LSCs) in order to overcome these deficiencies. Using a radiobased crossing control system as an example we outline how to embed LSCs into a modelbased development process. This entails a transition from scenariolike Sequence Charts used early in the design process to the graphical specification of system properties to be verified in later stages.},
xtopics = {lsc meth use} } 
[inproceedings] bibtexM. Lettrari, "Using Abstractions for Heuristic State Space Exploration of Reactive ObjectOriented Systems, pp. 462481.
@INPROCEEDINGS{Lettrari:2003,
author = {M. Lettrari},
title = {Using Abstractions for Heuristic State Space Exploration of Reactive ObjectOriented Systems},
booktitle = {FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 814, 2003, Proceedings},
year = {2003},
volume = {2805},
series = {Lecture Notes in Computer Science},
pages = {462481},
publisher = {Springer},
postscript = {lettrarie01.ps} } 
[incollection] bibtexA. Lüdtke, C. Möbus, R. Raabe, D. Eschrich, und T. Engwert, "Evaluationsbericht für das Trainingsprogramm SHAFT, Franke, G. und Selka, R., Eds., pp. 1218.
@INCOLLECTION{Luedtke_et_al2003,
author = {L{\"u}dtke, A. and M{\"o}bus, C. and Raabe, R. and Eschrich, D. and Engwert, T.},
title = {{Evaluationsbericht für das Trainingsprogramm SHAFT}},
booktitle = {{Strategische Handlungsflexibilität, CD zu Band II: Komplexität erkennen und bewältigen}},
publisher = {W.BertelsmannVerlag},
year = {2003},
editor = {G. Franke and R. Selka},
pages = {1218},
address = {Bielefeld},
owner = {luedtke},
timestamp = {2006.10.13} } 
[incollection] bibtexA. Lüdtke, C. Möbus, R. Raabe, D. Eschrich, und T. Engwert, "Erfahrungsberichte bzgl. des Trainingsprogramms SHAFT, Franke, G. und Selka, R., Eds., pp. 49, t1 s. 7–9, t2 s. 6, t3 s. 6.
@INCOLLECTION{Luedtke_et_al2003a,
author = {L{\"u}dtke, A. and M{\"o}bus, C. and Raabe, R. and Eschrich, D. and Engwert, T.},
title = {{Erfahrungsberichte bzgl. des Trainingsprogramms SHAFT}},
booktitle = {{Strategische Handlungsflexibilität, CD zu Band II: Komplexität erkennen und bewältigen}},
publisher = {W.BertelsmannVerlag},
year = {2003},
editor = {G. Franke and R. Selka},
pages = {49, T1 S. 79, T2 S. 6, T3 S. 68},
address = {Bielefeld},
owner = {luedtke},
timestamp = {2006.10.13} } 
[inproceedings] bibtexA. Metzner, "Incremental Task Allocation: Integrating RealTime Software in Distributed Embedded Systems.
@INPROCEEDINGS{metzner03,
author = {Alexander Metzner},
title = {{Incremental Task Allocation: Integrating RealTime Software in Distributed Embedded Systems}},
booktitle = {Proceeding of the $16^{th}$ International Conference on Software and Systems Engineering and their Application (ICSSEA'03)},
year = {2003} } 
[article] bibtexC. Möbus und A. Lüdtke, "ITS 2002 Tagungsbericht, pp. 4344
@ARTICLE{MoebusLuedtke2003,
author = {M{\"o}bus, C. and L{\"u}dtke, A.},
title = {{ITS 2002 Tagungsbericht}},
journal = {{KI Zeitschrift Künstliche Intelligenz}},
year = {2003},
volume = {1},
pages = {4344},
note = {ISSN 09331875},
booktitle = {KI Zeitschrift Künstliche Intelligenz},
owner = {luedtke},
timestamp = {2006.10.13} } 
[incollection] bibtexC. Möbus, A. Lüdtke, und H. J. Thole, "Hinweise zur Weiterentwicklung computersimulierter Planspiele, Franke, G. und Selka, R., Eds., pp. 139154.
@INCOLLECTION{MoebusLuedtkeThole2003,
author = {M{\"o}bus, C. and L{\"u}dtke, A. and Thole, H.J.},
title = {{Hinweise zur Weiterentwicklung computersimulierter Planspiele}},
booktitle = {{Strategische Handlungsflexibilität, Band 1: Grundlagen für die Entwicklung von Trainingsprogrammen}},
publisher = {W.BertelsmannVerlag},
year = {2003},
editor = {G. Franke and R. Selka},
pages = {139154},
address = {Bielefeld},
note = {ISBN 3763906525},
owner = {luedtke},
timestamp = {2006.10.13} } 
[article] bibtexE.R.~Olderog und H.~Dierks, "Moby/RT: A Tool for Specification and Verification of RealTime Systems, pp. 88105
@ARTICLE{OD03,
author = {E.R.~Olderog and H.~Dierks},
title = {{Moby/RT: A Tool for Specification and Verification of RealTime Systems}},
journal = {Journal of Universal Computer Science},
year = {2003},
volume = {9},
pages = {88105},
number = {2},
month = FEB } 
[incollection] bibtexO. Schröder, C. Möbus, und A. Lüdtke, "Individuelle Voraussetzungen der strategischen Handlungsflexibilität, Franke, G. und Selka, R., Eds., pp. 1780.
@INCOLLECTION{SchroederMoebusLuedtke2003,
author = {Schr{\"o}der, O. and M{\"o}bus, C. and L{\"u}dtke, A.},
title = {{Individuelle Voraussetzungen der strategischen Handlungsflexibilit{\"a}t}},
booktitle = {{Strategische Handlungsflexibilit{\"a}t, Band 1: Grundlagen f{\"u}r die Entwicklung von Trainingsprogrammen}},
publisher = {W.BertelsmannVerlag},
year = {2003},
editor = {G. Franke and R. Selka},
pages = {1780},
address = {Bielefeld},
note = {ISBN 3763906525} } 
[article] bibtexC. Schulte, M. Brörkens, I. Brückner, R. Buschermöhle, und T. Wolf, "Sicherheit für sicherheitskritische Systeme, pp. 1921
@ARTICLE{ees_verif:2003,
author = {C. Schulte and M. Brörkens and I. Brückner and R. Buschermöhle and T. Wolf},
title = {Sicherheit für sicherheitskritische Systeme},
journal = {{E}lectronic {E}mbedded {S}ysteme},
year = {2003},
volume = {09/03},
pages = {1921},
month = {September} } 
[proceedings] bibtexTools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003.
@PROCEEDINGS{LNCS2619, title = {{Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003}},
year = {2003},
editor = {H.~Garavel and J.~Hatcliff},
volume = {2619},
series = {Lecture Notes in Computer Science},
publisher = {SpringerVerlag} }
2002

[inproceedings] bibtexH.~Dierks und M.~Lettrari, "Constructing Test Automata from Graphical RealTime Requirements, pp. 433453.
@INPROCEEDINGS{DL02,
author = {H.~Dierks and M.~Lettrari},
title = {{Constructing Test Automata from Graphical RealTime Requirements}},
booktitle = {FTRTFT 2002},
year = {2002},
series = {Lecture Notes in Computer Science},
pages = {433453},
month = SEP, publisher = {SpringerVerlag},
crossref = {LNCS2469} } 
[inproceedings] bibtexJ. Bohn, W. Damm, J. Klose, A. Moik, und H. Wittke, "Modeling and Validating Train System Applications Using Statemate and Live Sequence Charts.
@INPROCEEDINGS{klose02c,
author = {J\"urgen Bohn and Werner Damm and Jochen Klose and Adam Moik and Hartmut Wittke},
title = {{M}odeling and {V}alidating {T}rain {S}ystem {A}pplications {U}sing {S}tatemate and {L}ive {S}equence {C}harts},
booktitle = {Proceedings of the Conference on Integrated Design and Process Technology ({IDPT2002})},
year = {2002},
editor = {H. Ehrig and B. J. Kr{\"a}mer and A. Ertas},
publisher = {Society for Design and Process Science},
abstract = {The European CENELEC norm now requires train system applications with critical safety integrity levels to be developed using formal methods, in particular supporting various forms of analysis to check for different correctness properties. In doing so, the CENELEC standard reflects the increasing need for advanced validation techniques in developing in particular also on board train system applications, which increasingly involve both complex and safety critical control units. This paper describes a methodology for developing train system applications based on powerful extensions of the Statemate modeling tool from ILogix Inc. The extension come in three dimensions:  Live Sequence Charts  a variant of the wellknown Message Sequence Charts of MSC2000 and the Sequence Diagrams in UML  are integrated with Statemate in order to allow capturing all interworkings between players such as onboard train control and train crossing control or between different trains, thus supporting the system development steps with a concise and semantically wellfounded representation of the critical communication protocols  Model Checking is integrated into Statemate to formally establish the correctness between such system requirements and a system specification developed in the industry standard CASE tool Statemate. This paper reports on an extension of the product version now marketed by ILogix, which supports formal verification of communication protocols captured as Live Sequence Charts. Model Checking can hence be used to verify all safety requirements on the system model, as well as to formally verify all system integration aspects using a virtual system integration as captured in Statemate.  Automatic Generation of Test Vectors from the Statemate specification model as well as from Scenarios can be used to validate the actual control units  in fact the test vectors can be downloaded to testrigs allowing hardwareintheloop tests of system components. The paper focuses on the overall methodology, which is explained using a trainsystem application, incorporating experiences from an ongoing cooperation with Bombardier transport systems.},
pdf = {klose02c.pdf} } 
[inproceedings] bibtex  Dokument aufrufenM. Brörkens und M. Möller, "Dynamic Event Generation for Runtime Checking using the JDI, pp. 2135.
@INPROCEEDINGS{broerkens02,
author = {Mark Br{\"o}rkens and Michael M{\"o}ller},
title = {Dynamic Event Generation for Runtime Checking using the {JDI}},
booktitle = {Runtime Verification},
year = {2002},
editor = {Klaus Havelund and Grigore Ro{\c{s}}u},
volume = {70},
series = {Electronic Notes in Theoretical Computer Science},
pages = {2135},
month = jul # { 26},
publisher = {Elsevier Science},
note = {Also DIKU technical report 0214 from University of Copenhagen. to appear.},
abstract = {Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level  either by inserting new source code prior to the compilation or by modifying the target code, e.g. Java byte code, before running the program. The jassda framework and tool enable runtime checking of Java programs against a CSPlike specification. For generating events it uses the Java Debug Interface (JDI) and thus no modifications to the code are necessary. Another advantage is that events are generated on demand, i.e. dynamically at runtime it is determined which events to generate for the current debug run without modifying the program itself. This paper shows how this event generation is done by the jassda framework.},
conference = {satellite workshop to CAV'02},
key = {RV},
postscript = {broerkens02.ps},
url = {http://jassda.sourceforge.net/publications.html},
venue = {Copenhagen, Denmark} } 
[inproceedings] bibtexW. Damm und B. Jonsson, "Eliminating Queues from RT UML Model Representations, pp. 375393.
@INPROCEEDINGS{Damm/Jonsson:2002,
author = {Werner Damm and Bengt Jonsson},
title = {Eliminating Queues from {RT UML} Model Representations },
booktitle = {7th Int'l Symposium on Formal Techniques in RealTime and Faul tTolerance Systems, FTRTFT 2002},
year = {2002},
editor = {Werner Damm and ErnstR{\"u}diger Olderog},
volume = {2469},
series = {LNCS},
pages = {375393},
month = {September},
publisher = {Springer} } 
[inproceedings] bibtexH.~Dierks, G.~Behrmann, und K.G.~Larsen, "Solving Planning Problems Using RealTime ModelChecking (Translating PDDL3 into Timed Automata), pp. 3039.
@INPROCEEDINGS{DBL02,
author = {H.~Dierks and G.~Behrmann and K.G.~Larsen},
title = {{Solving Planning Problems Using RealTime ModelChecking (Translating PDDL3 into Timed Automata)}},
booktitle = {{AIPSWorkshop Planning via ModelChecking}},
year = {2002},
editor = {F.~Kabanza and S.~Thiebaux},
pages = {3039},
month = APR } 
[inproceedings] bibtexH. Dierks und M. Lettrari, "Constructing Test Automata from Graphical RealTime Requirements, pp. 433453.
@INPROCEEDINGS{let02,
author = {Henning Dierks and Marc Lettrari},
title = {{C}onstructing {T}est {A}utomata from {G}raphical {R}eal{T}ime {R}equirements},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems},
year = {2002},
editor = {W. Damm and E.R. Olderog},
number = {2469},
series = {LNCS},
pages = {433453},
publisher = {Sprin\ger Ver\lag},
postscript = {let02.ps} } 
[inproceedings] bibtexM. Fränzle, "Take it NPeasy: Bounded Model Construction for Duration Calculus, pp. 245264.
@INPROCEEDINGS{fraenzle02b,
author = {Fr{\"a}nzle, Martin},
title = {Take it {NP}easy: Bounded Model Construction for Duration Calculus},
booktitle = {International Symposium on Formal Techniques in RealTime and FaultTolerant systems (FTRTFT 2002)},
year = {2002},
editor = {Olderog, ErnstR{\"u}diger and Damm, Werner},
volume = {2469},
series = {Lecture Notes in Computer Science},
pages = {245264},
publisher = {Springer Verlag},
abstract = {Following the recent successes of bounded modelchecking, we reconsider the problem of constructing models of discretetime Duration Calculus formulae. While this problem is known to be nonelementary when arbitrary length models are considered [Hansen1994], it turns out to be only NPcomplete when constrained to bounded length. As a corollary we obtain that model construction is in NP for the formulae actually encountered in case studies using Duration Calculus, as these have a certain smallmodel property. First experiments with a prototype implementation of the procedures demonstrate a competitive performance. \emph{Keywords:} Discretetime Duration Calculus; Model construction; Bounded model construction; Complexity},
postscript = {fraenzle02b.ps} } 
[article] bibtexM. Fränzle, "ModelChecking DenseTime Duration Calculus
@ARTICLE{Fraenzle:ModelCheckingDCFACS,
author = {Fr{\"a}nzle, Martin},
title = {ModelChecking DenseTime Duration Calculus},
journal = {Accepted for FACS},
year = {to appear 2002},
postscript = {fraenzle02a.ps} } 
[inproceedings] bibtexJ. Klose, T. Kropf, und J. Ruf, "A Visual Approach to Validating System Level Designs, pp. 186191.
@INPROCEEDINGS{klose02a,
author = {Jochen Klose and Thomas Kropf and J{\"u}rgen Ruf},
title = {A {V}isual {A}pproach to {V}alidating {S}ystem {L}evel {D}esigns},
booktitle = {15.th International Symposioum on System Synthesis (ISSS)},
year = {2002},
pages = {186  191},
address = {Kyoto, Japan},
publisher = {IEEE Computer Society Press},
abstract = {This paper proposes a simulationbased methodology for validation of a system under design in an early phase of development. The key element of this approach is the visual specification, as Live Sequence Charts (LSCs), of the properties to be checked. The LSCs are automatically translated into the input format for the SystemCbased checker engine, which indicates during simulation, if the property is fulfilled or produces a counterexample, if the property is violated. The entire process from the visual property specification to the checking is largely automated, which makes our approach accessible even for users which have not been trained in formal methods.} } 
[inproceedings] bibtexJ. Klose und B. Westphal, "Relating LSC Specifications to UML Models.
@INPROCEEDINGS{Klose/Westphal:2002,
author = {Jochen Klose and Bernd Westphal},
title = {Relating {LSC} {S}pecifications to {UML M}odels},
booktitle = {Proceedings INT2002 International Workshop on Integration of Specification Techniques for Applications in Engineering},
year = {2002},
editor = {Hartmut Ehrig and Martin GrosseRhode},
abstract = {Variants of sequence diagrams are used in UMLbased development processes to capture ``scenarios'', i.e. representative sequences of interactions between objects, to clarify usecases of the system under design. A set of scenarios provides a starting point for a formal specification to be verified. The sequence diagram variant SD of UML lacks formal rigor and expressivity so we propose to use Live Sequence Charts instead. Since the semantics of Live Sequence Charts is defined in terms of abstract ``instances'', the contribution of this work is to give an interpretation of LSCs with free variables. This is a single small step in an ongoing effort to establish a verification environment for UML models.},
postscript = {klose02b.ps.gz} } 
[conference] bibtexA. Lüdtke und C. Möbus, "Prognose von Bedienungsfehlern durch Simulation der Entstehung gelernter Sorglosigkeit bei der PilotCockpit Interaktion, pp. 163180.
@CONFERENCE{LuedtkeMoebus2002c,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{Prognose von Bedienungsfehlern durch Simulation der Entstehung gelernter Sorglosigkeit bei der PilotCockpit Interaktion}},
booktitle = {{Situation Awareness in der Fahrzeug und Prozessf{\"u}hrung: 44. Fachausschusssitzung Anthropotechnik der Deutschen Gesellschaft f{\"u}r Luft und Raumfahrt e.V}},
year = {2002},
editor = {M. Grandt and K.P. Gärtner},
number = {200204},
series = {DGLRBericht},
pages = {163180},
address = {Bonn},
publisher = {{Deutsche Gesellschaft f{\"u}r Luft und Raumfahrt e.V.}},
note = {ISBN 3932182294} } 
[conference] bibtexA. Lüdtke und C. Möbus, "Prognose von Bedienungsfehlern durch Routinebildung in teilautonomen Systemen: Konzept und empirische Untersuchung, pp. 164184.
@CONFERENCE{LuedtkeMoebus2002a,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{Prognose von Bedienungsfehlern durch Routinebildung in teilautonomen Systemen: Konzept und empirische Untersuchung}},
booktitle = {{Bedienen und Verstehen: 4. Berliner Werkstatt MenschMaschineSysteme 2001}},
year = {2002},
editor = {R. Marzi and V. Karavezyris and H.H. Erbe and K.P. Timpe},
pages = {164184},
address = {D{\"u}sseldorf},
publisher = {VDI Verlag GmbH},
note = {ISBN 318300822X} } 
[conference] bibtexA. Lüdtke und C. Möbus, "Modellierung von Routineeffekten durch gelernte Sorglosigkeit bei der Bedienung teilautonomer Systeme, p. 464.
@CONFERENCE{LuedtkeMoebus2002,
author = {L{\"u}dtke, A. and M{\"o}bus, C.},
title = {{Modellierung von Routineeffekten durch gelernte Sorglosigkeit bei der Bedienung teilautonomer Systeme}},
booktitle = {{43. Kongress der Deutschen Gesellschaft für Psychologie}},
year = {2002},
pages = {464},
address = {Lengerich},
publisher = {Pabst Science Publishers},
note = {ISBN 3936142882} } 
[inproceedings] bibtexA. Lüdtke, C. Möbus, und H. J. Thole, "Cognitive Modelling Approach to Diagnose OverSimplification in SimulationBased Training, pp. 496506.
@INPROCEEDINGS{LuedtkeMoebusThole2002,
author = {L{\"u}dtke, A. and M{\"o}bus, C. and Thole, H.J.},
title = {{Cognitive Modelling Approach to Diagnose OverSimplification in SimulationBased Training}},
booktitle = {{Proceedings of ITS2002 the 6th International Conference Intelligent Tutoring Systems, Biarritz, France and San Sebastian, Spain, June 2002}},
year = {2002},
editor = {St. A. Cerri and G. Gouarderes and F. Paraguacu},
volume = {2363},
series = {LNCS},
pages = {496506},
address = {Berlin},
publisher = {Springer},
note = {ISBN 3540437509} } 
[book] bibtexFormal Techniques in RealTime and FaultTolerant Systems, W.~Damm und E.R.~Olderog, Eds.
@BOOK{LNCS2469, title = {{Formal Techniques in RealTime and FaultTolerant Systems}},
publisher = {{SpringerVerlag}Verlag},
year = {2002},
editor = {W.~Damm and E.R.~Olderog},
volume = {2469},
series = {Lecture Notes in Computer Science} }
2001

[article] bibtex  Dokument aufrufenT. Bienmüller, W. Damm, J. Klose, und H. Wittke, "Formale Analyse und Verifikation von Statemate Entwürfen
@ARTICLE{itti00,
author = {Tom Bienm{\"u}ller and Werner Damm and Jochen Klose and Hartmut Wittke},
title = {Formale {A}nalyse und {V}erifikation von {S}tatemate {E}ntw{\"u}rfen},
journal = {it+ti},
year = {2001},
volume = {43},
number = {1},
url = {http://www.itti.de} } 
[inproceedings] bibtexU. Brockmeyer, J. Klose, und M. Lettrari, "UML Validation Suite.
@INPROCEEDINGS{klose01c,
author = {Udo Brockmeyer and Jochen Klose and Marc Lettrari},
title = {{UML V}alidation {S}uite},
booktitle = {Proceedings of {FATES'01}  {F}ormal {A}pproaches to {T}esting of {S}oftware},
year = {2001},
editor = {J. Tretmans and E. Brinksma},
postscript = {klose1c.ps.gz} } 
[article] bibtexW. Damm und M. Cohen, "Advanced Validation Techniques Meet Complexity Challange in Embedded Software Development
@ARTICLE{damm01b,
author = {Werner Damm and Moshe Cohen},
title = {Advanced Validation Techniques Meet Complexity Challange in Embedded Software Development},
journal = {Embedded Systems Journal},
year = {2001},
note = {(to appear)},
abstract = {While people seem willing to buy software for PCs that crashes regularly, embedded software in products like cars, trains, airplanes, cellular phones, switching systems, elevators, or medical devices must meet significantly higher product quality standards. To ensure high availability, the design process for embedded software must address the challenge of stringent timeto market and quality requirements in the face of an exponential growth both in function complexity and distribution. Advanced validation techniques are fast becoming essential in mastering this challenge.},
postscript = {damm01b.ps.gz} } 
[article] bibtexW. Damm und D. Harel, "LSCs: Breathing Life into Message Sequence Charts, pp. 4580
@ARTICLE{Damm01a,
author = {W. Damm and D. Harel},
title = {{LSC}s: {B}reathing {L}ife into {M}essage {S}equence {C}harts},
journal = {Formal {M}ethods in {S}ystem {D}esign},
year = {2001},
volume = {19},
pages = {45  80},
number = {1},
month = {July},
abstract = {While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively quite weak, being based on the modest semantic notion of a partial ordering of events as defined, e.g., in the ITU standard. A highly expressive and rigorously defined MSC language is a must for serious, semantically meaningful tool support for usecases and scenarios. It is also a prerequisite to addressing what we regard as one of the central problems in behavioral specification of systems: relating scenariobased interobject specification to statemachine intraobject specification. This paper proposes an extension of MSCs, which we call live sequence charts (or LSCs), since our main extension deals with specifying "liveness", i.e., things that must occur. In fact, LSCs allow the distinction between possible and necessary behavior both globally, on the level of an entire chart and locally, when specifying events, conditions and progress over time within a chart. This makes it possible to specify forbidden scenarios, and enables naturally specified structuring constructs like as subcharts, branching and iteration.},
editor = {A. Benveniste and A. Poigne} } 
[article] bibtexW. Damm und J. Klose, "Verification of a Radiobased Signaling System Using the Statemate Verification Environment
@ARTICLE{Klose01a,
author = {Werner Damm and Jochen Klose},
title = {Verification of a {R}adiobased {S}ignaling {S}ystem {U}sing the {S}tatemate {V}erification {E}nvironment},
journal = {Formal {M}ethods in {S}ystem {D}esign},
year = {2001},
volume = {19},
number = {2},
abstract = {With the trend to partially move safetyrelated features from courtyards into onboard control software, new challenges arise in supporting such designs by formal verification capabilities, essentially entailing the need for a modelbased design process. This paper reports on the usage of the Statemate Verification Environment to model and verify a radiobased signaling systems, a trial case study offered by the German train system company DB. It shows, that industrially sized applications can be modeled and verified with a verification tool to be offered as a commercial product by ILogix, Inc. },
editor = {Stefania Gnesi and Diego Latella} } 
[article] bibtexH.~Dierks und J.~Tapken, "Moby/PLC: Eine graphische Entwicklungsumgebung für SPSProgramme, pp. 3844
@ARTICLE{DT01,
author = {H.~Dierks and J.~Tapken},
title = {{Moby/PLC: Eine graphische Entwicklungsumgebung f{\"u}r SPSProgramme}},
journal = {atAutomatisierungstechnik},
year = {2001},
volume = {49},
pages = {3844},
number = {1} } 
[inproceedings] bibtexM. Fränzle, "What will be eventually true of polynomial hybrid automata, pp. 340359.
@INPROCEEDINGS{Fraenzle:WhatWillBeEventuallyTrueOfHybridAutomata,
author = {Fr{\"a}nzle, Martin},
title = {What will be eventually true of polynomial hybrid automata},
booktitle = {Theoretical Aspects of Computer Software (TACS 2001)},
year = {2001},
editor = {Kobayashi, Naoki and Pierce, Benjamin C.},
volume = {2215},
series = {LNCS},
pages = {340359},
publisher = {Springer Verlag},
abstract = {Hybrid automata have been introduced in both control engineering and computer science as a formal model for the dynamics of hybrid discretecontinuous systems. While computability issues concerning safety properties have been extensively studied, liveness properties have remained largely uninvestigated. In this article, we investigate decidability of state recurrence and of progress properties. First, we show that state recurrence and progress are in general undecidable for polynomial hybrid automata. Then, we demonstrate that they are closely related for hybrid automata subject to a simple model of noise, even though these automata are infinitestate systems. Based on this, we augment a semidecision procedure for recurrence with a semidecision method for lengthboundedness of paths in such a way that we obtain an automatic verification method for progress properties of linear and polynomial hybrid automata that may only fail on pathological, practically uninteresting cases. These cases are such that satisfaction of the desired progress property crucially depends on the complete absence of noise, a situation unlikely to occur in real hybrid systems.},
postscript = {fraenzle01b.ps} } 
[article] bibtexM. Fränzle und K. Lüth, "Visual Temporal Logic as a Rapid Prototyping Tool, pp. 93113
@ARTICLE{FraenzleLueth:VisualTLasRPToolJournal,
author = {Fr{\"a}nzle, Martin and L{\"u}th, Karsten},
title = {Visual Temporal Logic as a Rapid Prototyping Tool},
journal = {Computer Languages},
year = {2001},
volume = {27},
pages = {93113},
number = {13},
abstract = {Within this survey article, we explain realtime symbolic timing diagrams and the ICOS toolbox supporting timingdiagrambased requirements capture and rapid prototyping. Realtime symbolic timing diagrams are a fullfledged metrictime temporal logic, but with a graphical syntax reminiscent of the informal timing diagrams widely used in electrical engineering. ICOS integrates a variety of tools, ranging from graphical specification editors over tautology checking and counterexample generation to code generators emitting C or VHDL, thus bridging the gap from formal specification to rapid prototype generation.},
postscript = {fraenzle01a.ps} } 
[inproceedings] bibtexJ. Klose und M. Lettrari, "Scenariobased Monitoring and Testing of Realtime UML models.
@INPROCEEDINGS{klose01d,
author = {Jochen Klose and Marc Lettrari},
title = {Scenariobased {M}onitoring and {T}esting of {R}ealtime {UML} models},
booktitle = {{UML} 2001  {T}he {U}nified {M}odeling {L}anguage: {M}odeling {L}anguages, {C}oncepts, and {T}ools},
year = {2001},
editor = {M. Gogolla and C. Kobryn},
volume = {2185},
series = {LNCS},
publisher = {Springer Verlag},
abstract = {In this paper it is shown how Sequence Diagrams can be used both for monitoring and testing functional and realtime requirements of an executable UML design. We show how this testing approach can be integrated in an UMLbased development process. In addition, we will present how a prototype which implements the described monitoring and testing methods is integrated in a well known UML design tool.} } 
[inproceedings] bibtexJ. Klose und H. Wittke, "An Automata Based Representation of Live Sequence Charts.
@INPROCEEDINGS{Klose/Wittke:2001,
author = {Jochen Klose and Hartmut Wittke},
title = {An {A}utomata {B}ased {R}epresentation of {L}ive {S}equence {C}harts},
booktitle = {Proceedings of TACAS 2001},
year = {2001},
editor = {Tiziana Margaria and Wang Yi},
number = {2031},
series = {LNCS},
publisher = {Sprin\ger Ver\lag},
abstract = {The growing popularity of sequence charts, first of all Message Sequence Charts and UML Sequence Diagrams, for the description of communication behavior has evoked criticism regarding the semantics of the charts which led to extensions of these standardized visual formalisms. One such extension are Live Sequence Charts which allow to distinguish mandatory and possible behavior in protocol specifications. In the original language definition for LSCs the semantics are only described informally, although a sketch for a possible formalization has been provided as well. In this paper we intend to fill in the semantic blanks of the original LSC definition. Following the sketched path we define the semantics of an LSC by deriving a Timed Büchi Automata from it. We also consider qualitative and quantative timing aspects and subcharts.} } 
[techreport] bibtexC. Möbus und A. Lüdtke, "Eingebettete Systeme: Unterstützung der Sicherheitsanalyse von AvionikSystemen.,".
@TECHREPORT{MoebusLuedtke2001,
author = {M{\"o}bus, C. and L{\"u}dtke, A.},
title = {{Eingebettete Systeme: Unterstützung der Sicherheitsanalyse von AvionikSystemen.}},
institution = {{Oldenburger Forschungs und Entwicklungsinstitut für InformatikWerkzeuge und Systeme, Jahresbericht 2000}},
year = {2001},
owner = {luedtke},
pages = {2024},
timestamp = {2006.12.13} }
2000

[misc] bibtex  Dokument aufrufenT. Bienmüller, U. Brockmeyer, Hans Jürgen Holberg, und H. Wittke, Automatic Debugging for STATEMATE Designs.
@MISC{stmanw00,
author = {Tom Bienm{\"u}ller and Udo Brockmeyer and {Hans J{\"u}rgen Holberg} and Hartmut Wittke},
title = {Automatic {D}ebugging for {STATEMATE} {D}esigns},
year = {2000},
note = {8. {D}eutsches {A}nwenderforum f{\"u}r {STATEMATE} Magnum},
postscript = {stmanw00.ps.gz},
url = {http://www.bernermattner.de/news_events/UserGroupMeeting2000/analysis.pdf} } 
[inproceedings] bibtexT. Bienmüller, W. Damm, und H. Wittke, "The STATEMATE Verification Environment  Making it real, pp. 561567.
@INPROCEEDINGS{cav00,
author = {Tom Bienm{\"u}ller and Werner Damm and Hartmut Wittke},
title = {The {STATEMATE} {V}erification {E}nvironment  {M}aking it real},
booktitle = {12th international {C}onference on {C}omputer {A}ided {V}erification, {CAV}},
year = {2000},
editor = {E. Allen Emerson and A. Prasad Sistla},
number = {1855},
series = {LNCS},
pages = {561567},
publisher = {Springer Verlag},
abstract = {The STATEMATE Verification Environment supports requirement analysis and specification development of embedded controllers as part of the STATEMATE product offering of ILogix, Inc. This paper discusses key enhancements of the prototype tool in order to enable full scale industrial usage of the toolset. It thus reports on a successfully completed technology transfer from a prototype toolset to a commercial offering. The discussed enhancements are substantiated with performance results all taken from real industrial applications of leading companies in automotive and avionics.} } 
[inproceedings] bibtexH.~Dierks, "Specification and Verification of Polling RealTime Systems, pp. 3241.
@INPROCEEDINGS{Die00c,
author = {H.~Dierks},
title = {{Specification and Verification of Polling RealTime Systems}},
booktitle = {{Ausgezeichnete Informatikdissertationen 1999}},
year = {2000},
editor = {H.~Fiedler and O.~G{\"u}nther and W.~Grass and S.~H{\"o}lldobler and G.~Hotz and R.~Reischuk and B.~Seeger and D.~Wagner},
pages = {3241},
publisher = {Teubner} } 
[inproceedings] bibtexH.~Dierks, "A Process Algebra for RealTime Programs, pp. 6681.
@INPROCEEDINGS{Die00b,
author = {H.~Dierks},
title = {{A Process Algebra for RealTime Programs}},
booktitle = {FASE 2000: Fundamental Approaches to Software Engineering},
year = {2000},
editor = {T.~Maibaum},
volume = {1783},
series = {Lecture Notes in Computer Science},
pages = {6681},
publisher = {SpringerVerlag},
optcrossref = {LNCS1783} } 
[article] bibtexH.~Dierks, "PLCAutomata: A New Class of Implementable RealTime Automata, pp. 6193
@ARTICLE{Die00,
author = {H.~Dierks},
title = {{PLCAutomata: A New Class of Implementable RealTime Automata}},
journal = {Theoret.\ Comput.\ Sci.},
year = {2000},
volume = {253},
pages = {6193},
number = {1},
month = DEC, optnote = {full version of \cite{Die97}} } 
[article] bibtexH.~Dierks und J.~Tapken, "Modelling and Verifying of `CashPoint Service' Using Moby/PLC, pp. 221222
@ARTICLE{DT00,
author = {H.~Dierks and J.~Tapken},
title = {{Modelling and Verifying of `CashPoint Service' Using Moby/PLC}},
journal = {Formal Aspects of Computing},
year = {2000},
volume = {12},
pages = {221222} } 
[inproceedings] bibtexJ. Klose und A. Moik, "Modellierung der FORMSFallstudien mit Statemate.
@INPROCEEDINGS{klose00,
author = {Jochen Klose and Adam Moik},
title = {{M}odellierung der {FORMS}{F}allstudien mit {S}tatemate},
booktitle = {{FORMS2000}  {F}ormale {T}echniken f{\"u}r die {E}isenbahnsicherung},
year = {2000},
editor = {Eckehard Schnieder},
number = {441},
series = {Fortschritt{B}erichte {VDI} {R}eihe 12},
publisher = {{VDI} Verlag},
postscript = {klose00.ps.gz} } 
[article] bibtex  Dokument aufrufenA. Metzner und J. Niehaus, "MSPARC: Multithreading in RealTime Architectures, pp. 10341051
@ARTICLE{metzner2000,
author = {A. Metzner and J. Niehaus},
title = {MSPARC: Multithreading in RealTime Architectures},
journal = {Journal of Universal Computer Science},
year = {2000},
volume = {6},
pages = {10341051},
number = {10},
abstract = {This paper presents the use of multithreaded processors in realtime architectures. In particular we will handle realtime applications with hard timing constraints. In our approach, events (e.g. timer interrupts, signals from the environment, etc) are distinguished into three classes according to the reaction times that have to be met. Since two of these classes are well known in realtime systems, we will focus on the new class, for which the special features of a multithreaded processor together with a realtime scheduler realized in hardware are employed. Doing so enables us to realize the handling of events from this new class in software while still meeting the demands on reaction time. Additionally, the predictability of the application and the ease of implementing them are increased. The processor, named MSPARC, which we developed to support these features, is based on block multithreading and is outlined in this paper, too. We then present an architecture, designed for rapid prototyping of embedded systems, to show the feasibility of this approach. Finally, a case study shows the potential of multithreading for embedded systems.},
url = {http://www.jucs.org/jucs_6_10/msparc_multithreading_in_real} } 
[techreport] bibtexC. Möbus und A. Lüdtke, "Eingebettete Systeme: Wissensbasierte Unterstützung der Sicherheitsanalyse,".
@TECHREPORT{MoebusLuedtke2000,
author = {M{\"o}bus, C. and L{\"u}dtke, A.},
title = {{Eingebettete Systeme: Wissensbasierte Unterstützung der Sicherheitsanalyse}},
institution = {{Oldenburger Forschungs und Entwicklungsinstitut für InformatikWerkzeuge und Systeme, Jahresbericht 1999}},
year = {2000},
owner = {luedtke},
pages = {4043},
timestamp = {2006.12.13} } 
[article] bibtexJ. Niehaus, W. Damm, A. Metzner, und A. Mikschl, "Die EVENTSArchitektur, pp. 4044
@ARTICLE{events2000,
author = {J. Niehaus and W. Damm and A. Metzner and A. Mikschl},
title = {Die EVENTSArchitektur},
journal = {it + ti},
year = {2000},
volume = {42},
pages = {4044},
number = {2},
abstract = {Die innerhalb des EVENTS Projekts entwickelte Zielarchitektur ist auf eine möglichst große Reduktion der durch Taskwechsel entstehenden Latenzzeiten in eingebetteten Steuerungssystemen hin ausgerichtet. Dazu werden zum einen in einer Eigenentwicklung entstandene multithreaded Prozessoren (MSPARC) verwendet. Zum anderen wird ein neues Architekturkonzept realisiert, in dem diese Prozessoren als SlaveModule zu einem in Hardware realisiertem, externen Controller eingesetzt werden. In diesem Artikel beschreiben wir zunächst die im Projekt unterstützte Klasse von Applikationen und stellen dann die EVENTS Architektur vor. Eine erste Leistungsabschätzung mit kleinen Benchmarks läßt auf die zu erwartende Leistung des Systems schließen.} } 
[inproceedings] bibtexJ. Niehaus, K. Lüth, und W. Damm, "Multithreading in Rapid Prototyping Target Platforms, pp. 116122.
@INPROCEEDINGS{niehaus2000b,
author = {J{\"u}rgen Niehaus and Karsten L{\"u}th and Werner Damm},
title = {Multithreading in Rapid Prototyping Target Platforms},
booktitle = {AES2000},
year = {2000},
pages = {116122},
month = {Jan.},
publisher = {FZI Karslruhe},
abstract = {This paper describes work in progress on the use of multithreaded processors as a target platform for rapid prototyping of embedded control systems. We give a short introduction to multithreaded processors in general and the MSPARC  a SPARC V.8 based processor capable of multithreading with four contexts  in particular. A rapid prototyping target platform mainly consisting of a MSPARC processor and a FPGAfield is also presented. Finally, we show the design of an ignition control system used as a case study and present preliminary performance results of the architecture, which were obtained using an execution based, cycle accurate simulator.},
postscript = {niehaus2000b.ps} } 
[inproceedings] bibtexF. Terrier, N. Voros, und U. Brockmeyer, "Specification, Implementation, and Validation of ObjectOriented Embedded Systems, pp. 150177.
@INPROCEEDINGS{brockmeyer00a,
author = {F. Terrier and N. Voros and U. Brockmeyer},
title = {{Specification, Implementation, and Validation of ObjectOriented Embedded Systems}},
booktitle = {ObjectOriented Technology  ECOOP 2000 Workshop Reader},
year = {2000},
editor = {J. Malenfant, S. Moisan, A. Moreira},
volume = {1964},
series = {Lecture Notes in Computer Science},
pages = {150177},
abstract = {This workshop objective is to identify the main lacks of UML for developing realtime embedded systems and the main prospective directions for research to these difficulties. For that, it aims to gather academics and industrial people to discuss on industrial needs, on formalisms prospects and on advanced solutions. It tries to tackle the three main parts of a development cycle: specification/analysis, design/implementation and validation. Three main sessions have emerged from the workshop submissions. The first one was focused on setting the end users requirements for UML modeling of realtime embedded systems. The second has been focused on design and implementation techniques proposals and experiences. The third has been centered on formal techniques for the validation of the applications from their UML model. } }
vor 2000

[inproceedings] bibtexH.~Dierks, "PLCAutomata: A New Class of Implementable RealTime Automata, pp. 111125.
@INPROCEEDINGS{Die97,
author = {H.~Dierks},
title = {{PLCAutomata: A New Class of Implementable RealTime Automata}},
booktitle = {ARTS'97},
year = {1997},
volume = {1231},
series = {Lecture Notes in Computer Science},
pages = {111125},
month = MAY, publisher = {SpringerVerlag},
crossref = {LNCS1231},
optnote = {short version of \cite{Die00}} } 
[inproceedings] bibtexH.~Dierks, "Synthesising Controllers from RealTime Specifications, pp. 126133.
@INPROCEEDINGS{Die97b,
author = {H.~Dierks},
title = {{Synthesising Controllers from RealTime Specifications}},
booktitle = {{Tenth International Symposium on System Synthesis}},
year = {1997},
pages = {126133},
publisher = {IEEE Computer Society},
crossref = {ISSS97},
optmonth = {#SEP#},
optnote = {short version of \cite{Die99}} } 
[inproceedings] bibtexH.~Dierks, "The Production Cell: A Verified RealTime System, pp. 208227.
@INPROCEEDINGS{Die96,
author = {H.~Dierks},
title = {{The Production Cell: A Verified RealTime System}},
booktitle = {{Formal Techniques in RealTime and FaultTolerant Systems}},
year = {1996},
pages = {208227},
crossref = {LNCS1135} } 
[inproceedings] bibtexH.~Dierks und C.~Dietz, "Graphical Specification and Reasoning: Case Study ``Generalized Railroad Crossing'', pp. 2039.
@INPROCEEDINGS{DD97,
author = {H.~Dierks and C.~Dietz},
title = {{Graphical Specification and Reasoning: Case Study ``Generalized Railroad Crossing''}},
booktitle = {FME'97},
year = {1997},
editor = {J.~Fitzgerald and C.B.~Jones and P.~Lucas},
volume = {1313},
series = {Lecture Notes in Computer Science},
pages = {2039},
publisher = {SpringerVerlag},
crossref = {LNCS1313} } 
[inproceedings] bibtexH.~Dierks, A.~Fehnker, A.~Mader, und F.W.~Vaandrager, "Operational and Logical Semantics for Polling RealTime Systems, pp. 2940.
@INPROCEEDINGS{DFMV98,
author = {H.~Dierks and A.~Fehnker and A.~Mader and F.W.~Vaandrager},
title = {{Operational and Logical Semantics for Polling RealTime Systems}},
booktitle = {FTRTFT'98},
year = {1998},
volume = {1486},
series = {Lecture Notes in Computer Science},
pages = {2940},
publisher = {SpringerVerlag},
crossref = {LNCS1486},
optnote = {short version of \cite{DFMV98full}} } 
[inproceedings] bibtexH.~Dierks und M.~Schenke, "A Unifying Framework for Correct Program Construction, pp. 122150.
@INPROCEEDINGS{DS98,
author = {H.~Dierks and M.~Schenke},
title = {{A Unifying Framework for Correct Program Construction}},
booktitle = {Mathematics of Program Construction 98},
year = {1998},
editor = {J.~Jeuring},
volume = {1422},
series = {Lecture Notes in Computer Science},
pages = {122150},
month = JUN, publisher = {SpringerVerlag},
crossref = {LNCS1422} } 
[inproceedings] bibtexE.R.~Olderog und H.~Dierks, "Decomposing RealTime Specifications, pp. 465489.
@INPROCEEDINGS{OD98,
author = {E.R.~Olderog and H.~Dierks},
title = {{Decomposing RealTime Specifications}},
booktitle = {{Compositionality: The Significant Difference}},
year = {1998},
pages = {465489},
crossref = {LNCS1536} } 
[inproceedings] bibtexJ.~Tapken und H.~Dierks, "MOBY/PLC  Graphical Development of PLCAutomata, pp. 311314.
@INPROCEEDINGS{TD98,
author = {J.~Tapken and H.~Dierks},
title = {{MOBY/PLC  Graphical Development of PLCAutomata}},
booktitle = {FTRTFT'98},
year = {1998},
volume = {1486},
series = {Lecture Notes in Computer Science},
pages = {311314},
publisher = {SpringerVerlag},
crossref = {LNCS1486} } 
[inproceedings] bibtexA.~Allara, M.~Bombana, S.~Comai, B.~Josko, R.~Schlör, und D.~Sciuto, "Specification of Embedded Monitors for Property Checking, pp. 117126.
@INPROCEEDINGS{josko99a,
author = {A.~Allara and M.~Bombana and S.~Comai and B.~Josko and R.~Schl{\"o}r and D.~Sciuto},
title = {Specification of Embedded Monitors for Property Checking},
booktitle = {Proceedings, Forum on Design Languages, {FDL'99}},
year = {1999},
pages = {117126},
abstract = {In the formal verification domain the use of monitors represents a powerful technique where model I/O sequences are monitored and triggers are raised to allow a simplification in the construction of formal properties. This reduces the chances of incorrect system specifications and can sometimes reduce also the actual model checking time. The drawback of this technique lies in its heterogeneity. In fact, usually monitors are defined at the implementation level of the device model under test. In this paper we present a more general approach based on the idea of abstracting monitors definition from the model level up to the specification level without imposing further constraints on the current model checking techniques. A test case from the telecom domain is used to illustrate the definition and use of this type of embedded monitors, showing advantages and benefits related to their application. },
keywords = {Formal Verification, Monitors, Timing Diagrams, Model Checking} } 
[incollection] bibtexT. Bienmüller, J. Bohn, H. Brinkmann, U. Brockmeyer, W. Damm, H. Hungar, und P. Jansen, "Verification of Automotive Control Units, Olderog, E. und Steffen, B., Eds., pp. 319341.
@INCOLLECTION{csd99,
author = {Tom Bienm{\"u}ller and J{\"u}rgen Bohn and Henning Brinkmann and Udo Brockmeyer and Werner Damm and Hardi Hungar and Peter Jansen},
title = {Verification of Automotive Control Units},
booktitle = {Correct System Design},
publisher = {Springer Verlag},
year = {1999},
editor = {ErnstR{\"u}diger Olderog and Bernd Steffen},
volume = {1710},
series = {LNCS},
pages = {319341},
abstract = {This paper describes the application of modelchecking based verification tools to specification models of automotive control units. It firstly discusses the current state of a tool set which copes with discrete controllers described in \textsc{Statemate},
and then reports on proposed extensions currently under development to deal with hybrid ones which involve continuous values, too. First results based on an extension of abstraction techniques to verify such units are reported.},
postscript = {csd99.ps.gz} } 
[inproceedings] bibtexT. Bienmüller, U. Brockmeyer, W. Damm, G. Döhmen, C. Eßmann, H. Holberg, H. Hungar, B. Josko, R. Schlör, G. Wittich, H. Wittke, G. Clements, J. Rowlands, und E. Sefton, "Formal Verification of an Avionics Application using Abstraction and Symbolic Model Checking, pp. 150173.
@INPROCEEDINGS{sms99,
author = {Tom Bienm{\"u}ller and Udo Brockmeyer and Werner Damm and Gert D{\"o}hmen and Claus E{\ss}mann and HansJ{\"u}rgen Holberg and Hardi Hungar and Bernhard Josko and Rainer Schl{\"o}r and Gunnar Wittich and Hartmut Wittke and Geoffrey Clements and John Rowlands and Eric Sefton},
title = {Formal {V}erification of an {A}vionics {A}pplication using {A}bstraction and {S}ymbolic {M}odel {C}hecking},
booktitle = {Towards {S}ystem {S}afety  {P}roceedings of the {S}eventh {S}afetycritical {S}ystems {S}ymposium, Huntingdon, UK},
year = {1999},
editor = {Felix Redmill and Tom Anderson},
pages = {150173},
organization = {Safety{C}ritical {S}ystems {C}lub},
publisher = {Springer},
abstract = { This paper demonstrates the use of modelchecking based verification technology to establish safety critical properties for an industrial avionics application. The verification technology is tightly integrated with the Statemate system of iLogix Inc., USA. Key features of this technology are its scalability to complete system verification, the powerful debugging capabilities, graphical entry for safety critical properties, and the capability to reuse verification results for design components. The paper describes the application, the Statemate verification environment, and its use to establish safety critical properties of a British Aerospace application. The technical focus is on the use of abstraction techniques, allowing to focus verification on aspects of the design relevant to the property under investigation.},
postscript = {sms99.ps.gz} } 
[phdthesis] bibtexJ. Bohn, "Mechanical Support and Validation of a Design Calculus for Communicating Systems by a LogicBased Proof System,".
@PHDTHESIS{BohnPhD97,
author = {J\"urgen Bohn},
title = {Mechanical Support and Validation of a Design Calculus for Communicating Systems by a LogicBased Proof System},
school = {Department of Computer Science, University of Oldenburg},
year = {1997},
address = {Germany},
pages = {308},
postscript = {BohnPhD97.ps.gz} } 
[incollection] bibtexJ. Bohn und H. Hungar, "TRAVERDI  Transformation and Verification of Distributed Systems, Broy, M. und Jähnichen, S., Eds., pp. 317338.
@INCOLLECTION{hungar:BoHu95,
author = {J. Bohn and H. Hungar},
title = {TRAVERDI  Transformation and Verification of Distributed Systems},
booktitle = {KORSO: Methods, Languages, and Tools for the Construction of Correct Software},
publisher = {Springer},
year = {1995},
editor = {M. Broy and S. J\"ahnichen},
series = {LNCS 1009},
pages = {317338},
key = {BoHu95} } 
[inproceedings] bibtexJ. Bohn, " "Formalizing the transformational design of communicating systems in the theorem prover LAMBDA" , p. 14.
@INPROCEEDINGS{BohnHOA93,
author = {J{\"u}rgen Bohn},
title = {{ "Formalizing the transformational design of communicating systems in the theorem prover LAMBDA" }},
booktitle = {Higher Order Algebra, Logic and Term Rewriting (HOA'93)},
year = {1993},
editor = {J. Heering and K. Meinke and B. M{\"o}ller},
pages = {14},
month = sep, publisher = {CWI, Amsterdam, The Netherlands},
abstract = { },
postscript = {BohnHOA93.ps.gz} } 
[inproceedings] bibtexJ. Bohn, " "Formal transformational reasoning about reactive systems in the theorem prover LAMBDA" , p. 17.
@INPROCEEDINGS{BohnHOL94,
author = {J{\"u}rgen Bohn},
title = {{ "Formal transformational reasoning about reactive systems in the theorem prover LAMBDA" }},
booktitle = {Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications},
year = {1994},
editor = {T. Melham and J. Camilleri},
pages = {17},
publisher = {University of Malta},
abstract = { },
postscript = {BohnHOL94.ps.gz} } 
[inproceedings] bibtexJ. Bohn, W. Damm, O. Grumberg, H. Hungar, und K. Laster, " "FirstOrderCTL Model Checking" , pp. 283294.
@INPROCEEDINGS{BohnDammHungar98,
author = {J{\"u}rgen Bohn and Werner Damm and Orna Grumberg and Hardi Hungar and Karen Laster},
title = {{ "FirstOrderCTL Model Checking" }},
booktitle = {FSTTCS},
year = {1998},
volume = {1530},
series = {Lecture Notes in Computer Science},
pages = {283294},
month = {May},
abstract = {This work presents a firstorder model checking procedure that verifies systems with potentially infinite data spaces with respect to firstorder CTL specification. The procedure relies on a partition of the system variables into \emph{control} and \emph{data}. While control values are expanded into BDDrepresentations, data values enter in form of their properties relevant to the verification task. The algorithm is completely automatic. If the algorithm terminates, it has generated a firstorder verification condition on the data space which characterizes the system's correctness. Termination can be guaranteed for a class that properly includes the data independent systems, defined in \cite{Wol86}. The procedure works like a symbolic model checker on the control part. The data part is handled by annotating each controlexpanded state of the system by a firstorder formula. These formulas characterize, for each state, the set of data valuations that altogether make the specification true for the system. A novel part of our work is that the firstorder annotations are represented as BDDs and are manipulated symbolically. Since the formulas are represented by BDDs, we get ''for free'' propositional simplifications. Moreover, the canonical representation provided by BDDs makes it easier to detect termination of our model checking procedure. Finally, the encoding of predicates as boolean variables enables \emph{sharing} of subformulas among the formulas produced by the model checking procedure. This work improves \cite{DHGcharme95},
where we extended \emph{explicit} model checking algorithms. In contrast, this paper shows how to cast firstorder model checking into BDDbased representations. Thus, for complex control aspects of the design the full power of symbolic model checking is provided, while at the same time temporal reasoning is supported by the generation of a verification condition in cases where the data complexity is too high for ordinary procedures.},
issn = {03029743},
postscript = {BohnDammHungar98.ps.gz} } 
[inproceedings] bibtexJ. Bohn und W. Janssen, "A strategic approach to transformational design, pp. 609628.
@INPROCEEDINGS{BohnJanssen96,
author = {J{\"u}rgen Bohn and Wil Janssen},
title = {{A strategic approach to transformational design}},
booktitle = {Proc. Int. Conf. FME 96; Industrial benefit and Advances in Formal Methods},
year = {1996},
editor = {M. Gaudel and J. Woodcock},
volume = {1051},
series = {Lecture Notes in Computer Science},
pages = {609628},
address = {Oxford, UK},
month = mar, publisher = {SpringerVerlag, Berlin},
abstract = { },
postscript = {BohnJanssen96.ps.gz} } 
[inproceedings] bibtexJ. Bohn und S. Rössig, "On Automatic and Interactive Design of Communicating Systems, pp. 216237.
@INPROCEEDINGS{BohnRoessig95,
author = {J{\"u}rgen Bohn and Stephan R{\"o}ssig},
title = {On Automatic and Interactive Design of Communicating Systems},
booktitle = {Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95)},
year = {1995},
editor = {E. Brinksma and W. R. Cleaveland and K. G. Larsen and T. Margaria and B. Steffen},
volume = {1019},
series = {Lecture Notes in Computer Science},
pages = {216237},
address = {Aarhus, Denmark},
publisher = {SpringerVerlag},
issn = {03029743},
postscript = {BohnRoessig95.ps.gz} } 
[phdthesis] bibtexU. Brockmeyer, "Verifikation von STATEMATE Designs,".
@PHDTHESIS{brockmeyer99a,
author = {Udo Brockmeyer},
title = {Verifikation von STATEMATE Designs},
school = {CarlvonOssietzky Universit\"at Oldenburg},
year = {1999},
address = {Oldenburg},
month = {Dezember},
note = {Nr. 16/99  ISSN 09462910},
postscript = {brockmeyer99a.ps.gz} } 
[inproceedings] bibtexU. Brockmeyer und G. Wittich, "RealTime Verification of STATEMATE Designs  ToolPaper, pp. 537541.
@INPROCEEDINGS{brockmeyer98b,
author = {U. Brockmeyer and G. Wittich},
title = {{RealTime Verification of STATEMATE Designs  ToolPaper}},
booktitle = {Computer Aided Verification},
year = {1998},
editor = {Alan J. Hu and Moshe Y. Vardi},
volume = {1427},
series = {Lecture Notes in Computer Science},
pages = {537541},
abstract = {This toolpaper presents a toolset for realtime verification of STATEMATE designs. STATEMATE is a widely used design tool for embedded control applications. In our approach designs including all timing information are translated into untimed finite state machines (FSMs) %Kripke Structures which are verified by symbolic modelchecking. Realtime requirements are expressed by TCTL formulae interpreted over discrete time. A reduction from TCTL modelchecking to CTL modelchecking is implemented in order to use a CTL modelchecker for the verification task. Some experimental results of the toolset are given. },
postscript = {brockmeyer98b.ps} } 
[inproceedings] bibtexU. Brockmeyer und G. Wittich, "Tamagotchis Need Not Die  Verification of STATEMATE Designs, pp. 217231.
@INPROCEEDINGS{brockmeyer98a,
author = {U. Brockmeyer and G. Wittich},
title = {{Tamagotchis Need Not Die  Verification of STATEMATE Designs}},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
year = {1998},
editor = {Bernhard Steffen},
volume = {1384},
series = {Lecture Notes in Computer Science},
pages = {217231},
abstract = {This paper presents a toolset we built for supporting verification of STATEMATE designs. STATEMATE is a widely used design tool for embedded control applications. Designs are translated into finite state machines which are optimized and then verified by symbolic model checking. To express requirement specifications the visual formalism of symbolic timing diagrams is used. Their semantics is given by translation into temporal logic. If the model checker generates a counterexample, it is retranslated into either a symbolic timing diagram or a stimulus for the STATEMATE simulator. },
postscript = {brockmeyer98a.ps} } 
[inproceedings] bibtexU. Brockmeyer und G. Wittich, "Case Study: Verification of an Embedded FaultTolerant Avionics System, pp. 9095.
@INPROCEEDINGS{brockmeyer98d,
author = {U. Brockmeyer and G. Wittich},
title = {{Case Study: Verification of an Embedded FaultTolerant Avionics System}},
booktitle = {IEEE International Workshop on Embedded FaultTolerant Systems (EFTS'98)},
year = {1998},
pages = {9095},
abstract = {This paper shows how an faulttolerant avionics system given as a STATEMATE design can be verified using a toolset we built. We demonstrate our verification environment on a sample avionics case study which is provided by our project partner ESG. This case study is about a faulttolerant Helicopter Monitoring System of a Helicopter with two engines. There are two independent tasks which are scheduled periodically by a control task. For each engine the first task compares a computed and a measured rotations per minute (rpm) value. If the difference raises above a given threshold, the task generates an alarm displayed to the pilot. Then the pilot has to decide whether to switch off the engine or not. The second task monitors the remaining fuel of the aircraft. It first computes two values to determine the remaining amount of fuel. One value is computed by fuel throughput and one is computed by the initial amount of fuel and the flight distance. Again an alarm is generated if the two values differ too much. Otherwise the weighted average of these values is assumed to be the remaining amount of fuel. An alarm is also generated if this value reaches a critical threshold. All generated alarms have to be acknowledged by the pilot. The control task schedules the above two tasks and also accepts commands given by the pilot by performing the corresponding actions. We present some results we got on verifying some relevant properties of the faulttolerant monitoring system with our toolset. },
postscript = {brockmeyer98d.ps} } 
[inproceedings] bibtexC. Courcoubetis, W. Damm, und B. Josko, "Verification of timing properties of VHDL, pp. 225236.
@INPROCEEDINGS{josko93a,
author = {C. Courcoubetis and W. Damm and B. Josko},
title = {Verification of timing properties of {VHDL}},
booktitle = {5th Conference on ComputerAided Verification},
year = {1993},
editor = {C. Courcoubetis},
series = {Lecture Notes in Computer Science 697},
pages = {225236},
publisher = {SpringerVerlag},
abstract = {This paper shows how timing properties of VHDL processes can be verified using timed transition systems. The timing model being adopted is the timed automaton model used in the timing extension of Kurshan's COSPAN system. It demonstrates how a VHDL process can be translated into a timed automaton by describing the construction of the corresponding timed process that handles the scheduled signal assignments of the VHDL specification. Verification is performed in the case in which the complement of the timing properties to be verified are provided in terms of a timed automaton. Interestingly enough, this is the case for a large class of hardware properties expressed in terms of timing diagrams.} } 
[inproceedings] bibtexW. Damm, U. Brockmeyer, H. J. Holberg, G. Wittich, und M. Eckrich, "Einsatz formaler Methoden zur Erhöhung der Sicherheit eingebetteter Systeme im Kfz, pp. 349366.
@INPROCEEDINGS{brockmeyer97a,
author = {W. Damm and U. Brockmeyer and H.J. Holberg and G. Wittich and M. Eckrich},
title = {{Einsatz formaler Methoden zur Erh\"ohung der Sicherheit eingebetteter Systeme im Kfz}},
booktitle = {Systemengeneering in der KfzEntwicklung},
year = {1997},
editor = {VDIGesellschaft Fahrzeug und Verkehrstechnik},
volume = {1374},
series = {VDI Berichte},
pages = {349366},
abstract = { },
postscript = {brockmeyer97a.ps} } 
[inproceedings] bibtexW. Damm, G. Döhmen, V. Gerstner, und B. Josko, "Modular verification of Petri nets: The temporal logic approach, pp. 180207.
@INPROCEEDINGS{josko90b,
author = {Werner Damm and Gert D{\"o}hmen and Volker Gerstner and Bernhard Josko},
title = {Modular verification of Petri nets: The temporal logic approach},
booktitle = {Stepwise Refinement of Distributed Systems. {Models, Formalisms, Correctness}},
year = {1990},
editor = {Jaco W. de Bakker and WillemPaul de Roever and Grzegorz Rozenberg},
series = {Lecture Notes in Computer Science 430},
pages = {180207},
publisher = {SpringerVerlag},
abstract = {``How does reactive behaviour decompose? What can be done to encourage stepwise refinement of the behavioural aspects of a system? How can one cope with the intricacy, that the behaviour of a complex reactive system presents?'' These questions posed in [Harel, Pnueli 1985] and informally discussed there in the setting of statecharts, are taken up in this paper using a particular class of PetriNets as models for {\em open reactive systems}. It presents an assumption/commitment style temporal logic for specifying the behaviour of such systems, an automatic proof method for verifying the correctness of an implementation of such a specification in terms of the considered class of PetriNets based on model checking of MCTL formula, and presents a proofmethod for inferring the behaviour of a compound reactive system from the behaviour of its constituents. } } 
[inproceedings] bibtexW. Damm, G. Döhmen, und J. Klose, "Secure Decentralized Control of Railway Crossings, pp. 115132.
@INPROCEEDINGS{Klose99a,
author = {W. Damm and G. D{\"o}hmen and J. Klose},
title = {Secure Decentralized Control of Railway Crossings},
booktitle = {Fourth International {ERCIM} Workshop on Formal Methods in Industrial Critical Systems},
year = {1999},
editor = {S. Gnesi and D. Latella},
pages = {115  132},
abstract = { This paper demonstrates the use of model checking based verification technology to establish safety critical properties for a railway control application. The verification technology is tightly integrated with the Statemate system of iLogix Inc., USA. Key features of this technology are the powerful debugging capabilities and graphical entry for safety critical properties. This paper gives an overview over the verification environment and also highlights the design methodology that provides its base. In order to further enhance the verification environment we add Message Sequence Charts (MSC) to the existing toolset. We show that MSCs can be effectively used in the requirements analysis phase of the design process. As a sample application serves a railway control system.},
postscript = {klose99a.ps.gz} } 
[inproceedings] bibtexW. Damm und D. Harel, "LSCs: Breathing Life into Message Sequence Charts.
@INPROCEEDINGS{werner98a,
author = {W. Damm and D. Harel},
title = {{LSCs: Breathing Life into Message Sequence Charts}},
booktitle = {FMOODS'99 IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open ObjectBased Distributed Systems},
year = {1999},
abstract = {While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively quite weak, being based on the modest semantic notion of a partial ordering of events as defined, e.g., in the ITU standard. A highly expressive and rigorously defined MSC language is a must for serious, semantically meaningful tool support for usecases and scenarios. It is also a prerequisite to addressing what we regard as one of the central problems in behavioral specification of systems: relating scenariobased interobject specification to statemachine intraobject specification. This paper proposes an extension of MSCs, which we call live sequence charts (or LSCs), since our main extension deals with specifying "liveness", i.e., things that must occur. In fact, LSCs allow the distinction between possible and necessary behavior both globally, on the level of an entire chart and locally, when specifying events, conditions and progress over time within a chart. This also makes it possible to specify forbidden scenarios, and strengthens structuring constructs like as subcharts, branching and iteration.},
postscript = {werner98a.ps} } 
[incollection] bibtexW. Damm, H. Hungar, P. Kelb, und R. Schlör, "Using graphical specification languages and symbolic model checking in the verification of a production cell, Lewerentz, C. und Lindner, T., Eds., pp. 131149.
@INCOLLECTION{hungar:DHKS94,
author = {W. Damm and H. Hungar and P. Kelb and R. Schl\"or},
title = {Using graphical specification languages and symbolic model checking in the verification of a production cell},
booktitle = {Formal Development of Reactive Systems. Case Study Production Cell},
publisher = {Springer},
year = {1994},
editor = {C. Lewerentz and T. Lindner},
series = {LNCS 891},
pages = {131149},
key = {DHKS94} } 
[inproceedings] bibtexW. Damm, B. Josko, H. Hungar, und A. Pnueli, "A Compositional Realtime Semantics of STATEMATE Designs, pp. 186238.
@INPROCEEDINGS{DammJoskoHungarPnueli98,
author = {Werner Damm and Bernhard Josko and Hardi Hungar and Amir Pnueli},
title = {A Compositional Realtime Semantics of {STATEMATE} Designs},
booktitle = {Proceedings COMPOS'97},
year = {1998},
editor = {W.P.~de~Roever and H.~Langmaack and A.~Pnueli},
series = {Lecture Notes in Computer Science 1536},
pages = {186238},
publisher = {SpringerVerlag},
abstract = {This paper presents a reference semantics for a verification tool currently under development allowing to verify temporal properties of embedded control systems modelled using the STATEMATE system. The semantics reported differs from others reported in the literature by faithfully modelling the semantics as supported in the STATEMATE simulation tool. It differs from the recent paper by Harel and Naamad by providing a {\em compositional\/} semantics, a prerequisite for the support of {\em compositional verification methods},
and by the degree of mathematical rigour. We use a variant of \textit{synchronous transition systems} introduced by Manna and Pnueli as base model for our semantics. \par The STATEMATE modelling language constructs covered in this paper are \textit{Activity charts},
modelling the functional decomposition of a design into subunits called \textit{activities} as well as the \textit{information flow} between these, and \textit{Statecharts},
modelling reactive behaviour using the well established approach of hierarchically organized statemachines. We strive for a verification approach which is compositional w.r.t.\ the decomposition of systems into subsystems. This will allow activities of ``reasonable'' complexity to be verified using \textit{symbolic model checking}. \par Larger activities will be verified on the basis of proofsystems relating properties of individual activities to properties of compound activities, using the well known \textit{assumption commitment paradigm}. A key topic for this paper is the construction of so called \textit{compositional models},
which are ``rich enough'' to model the STATEMATE parallel composition by intersection of the infinite traces generated by the components of the parallel composition. Roughly, compositional models have to provide room for padding arbitrary (but still ``legal'') environment interactions into computations of a component. Alternatively, the construction of compositional models can be phrased as a requirement on the model to support a sufficiently rich class of \textit{observables} for assumptioncommitment style reasoning to be complete. In this sense, this paper derives the set of atomic propositions included as observables in the assumptioncommitment style temporal logic supported by the verification tool. \par The richness of the STATEMATE modelling languages forbids a complete treatment within such a formal semantics. While Harel and Naamad elaborate in a detailed fashion the construction of compound transitions from transition segments, we take this as given in this paper. We also abstract from the concrete syntax of action annotations, but keep them rich enough to show how all the associated intricacies can be handled formally.} } 
[incollection] bibtexW. Damm, B. Josko, und R. Schlör, "Specification and Verification of VHDLbased SystemLevel Hardware Designs, Börger, E., Ed., pp. 331410.
@INCOLLECTION{josko95,
author = {Werner Damm and Bernhard Josko and Rainer Schl{\"o}r},
title = {Specification and Verification of {VHDL}based SystemLevel Hardware Designs},
booktitle = {Specification and Validation Methods},
publisher = {Oxford University Press},
year = {1995},
editor = {E. B{\"o}rger},
pages = {331410},
abstract = {This chapter provides the semantic foundation of a formal verification environment for VHDL. The envisaged tool supports {\it specification\/} of systemlevel hardware designs using an extension of the classical concepts of timing diagrams allowing us to express firstorder properties and causality relations between events. A formal semantics of such {\it symbolic timing diagrams\/} is given in terms of a linear time firstorder temporal logic. Systemlevel designs expressed in VHDL  an IEEE standard hardware description language  can be verified against temporal logic specifications using a {\it compositional proof system\/} presented in this chapter. This proofsystem is proved correct with respect to a {\it formal semantics\/} for VHDL in the style of {\it structural operational semantics\/} based on {\it transition systems\/}. For the special case of VHDL designs using finite data types only, the semantics provides a link to {\it modelchecking\/} tools allowing {\it automatic verification\/} of VHDL designs against a temporal logic specification. Such a verification environment is currently under development within the ESPRIT project FORMAT.},
keywords = {VHDL, hardware verification, temporal logic, specification languages, formal semantics, visual formalisms} } 
[inproceedings] bibtexW. Damm, B. Josko, und R. Schlör, "A NetBased Semantics for VHDL, pp. 514519.
@INPROCEEDINGS{josko93b,
author = {W. Damm and B. Josko and R. Schl{\"o}r},
title = {A NetBased Semantics for {VHDL}},
booktitle = {Proceedings EURODAC with EUROVHDL 93},
year = {1993},
pages = {514519},
abstract = {The VHDL standard [IEEE87] gives only an informal description of the semantics of VHDL. But to apply formal verification techniques a precise semantics definition is necessary. This paper defines a formal semantics for VHDL based on interpreted Petri nets. The presented semantics is compositional and provides a link to automatic verification methods for VHDL based designs.} } 
[inproceedings] bibtexW. Damm, F. Liu, und T. Peikenkamp, "A graph Rewriting Model enhanced with sharing for ORparallel execution of Logic Programs, pp. 2946.
@INPROCEEDINGS{DLP91,
author = {W. Damm and F. Liu and T. Peikenkamp},
title = { A graph Rewriting Model enhanced with sharing for ORparallel execution of Logic Programs},
booktitle = {Proc. of SemaGraph'91 Symposium on the Semantics and Progmatics of Generalized Graph Rewriting},
year = {1991},
pages = {2946},
address = {Nijmegen, The Netherlands},
month = {December},
abstract = {This paper seeks for a further rise in efficiency of ORparallel execution models by exploiting sharing among different ORparallel processes. Inspired by the principle of graph rewriting for handling sharing in functional languages, we present a graph rewriting model enhanced with sharing for ORparallel execution of logic programs. Our approach is in orthogonal to most of the existing ORparallel models such as SRI, Aurora and Andorra models which aim to raise efficiency of ORparallel execution by incorporating different strategies for process control and environment management. The preliminary simulation results of the model enhanced with sharing have shown a significant reduction of computation tree and heap space used for the evaluation of nondeterministic programs. More importantly, comparied with nonshared ORparallel models, our model enhanced with sharing promises a speed up for nondeterministic programs.} } 
[inproceedings] bibtexW. Damm und A. Pnueli, "Verifying outoforder executions, pp. 2347.
@INPROCEEDINGS{damm97,
author = {W. Damm and A. Pnueli},
title = {Verifying outoforder executions},
booktitle = {Advances in Hardwre Design and Verification: IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods (CHARME)},
year = {1997},
editor = {H.F.Li and D.K.Probst},
pages = {2347},
publisher = {Chapman \& Hall} } 
[inproceedings] bibtexW. Damm, A. Pnueli, und S. Ruah, "Herbrand automata for hardware verification.
@INPROCEEDINGS{damm98,
author = {W. Damm and A. Pnueli and S. Ruah},
title = {Herbrand automata for hardware verification},
booktitle = {Proc of the 9th International Conference on Conucrrency (CONCUR)},
year = {1998},
editor = {R. De Simone and D. Sangiorgi},
series = {LNCS},
publisher = {Springer Verlag} } 
[article] bibtexH.~Dierks, "Synthesizing Controllers from RealTime Specifications, pp. 3343
@ARTICLE{Die99,
author = {H.~Dierks},
title = {{Synthesizing Controllers from RealTime Specifications}},
journal = {IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems},
year = {1999},
volume = {18},
pages = {3343},
number = {1} } 
[phdthesis] bibtexH.~Dierks, "Specification and Verification of Polling RealTime Systems,".
@PHDTHESIS{Die99b,
author = {H.~Dierks},
title = {{Specification and Verification of Polling RealTime Systems}},
school = {University of Oldenburg},
year = {1999},
month = JUL, optnote = {to appear} } 
[inproceedings] bibtexH.~Dierks, "Comparing ModelChecking and Logical Reasoning for RealTime Systems, pp. 1322.
@INPROCEEDINGS{Die98,
author = {H.~Dierks},
title = {{Comparing ModelChecking and Logical Reasoning for RealTime Systems}},
booktitle = {ESSLLI'98},
year = {1998},
pages = {1322},
note = {Workshop proceedings} } 
[mastersthesis] bibtexH.~Dierks, "Der Einsatz von TheoremBeweisern am Beispiel der Graphentheorie,".
@MASTERSTHESIS{Die97e,
author = {H.~Dierks},
title = {{Der Einsatz von TheoremBeweisern am Beispiel der Graphentheorie}},
school = {University of Oldenburg, Department of Mathematics, Oldenburg, Germany},
year = {1997},
month = AUG } 
[mastersthesis] bibtexH.~Dierks, "Die Fertigungszelle als verifiziertes Realzeitsystem,".
@MASTERSTHESIS{Die95,
author = {H.~Dierks},
title = {{Die Fertigungszelle als verifiziertes Realzeitsystem}},
school = { University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
year = {1995},
month = MAY, key = {T1} } 
[techreport] bibtexH.~Dierks, A.~Fehnker, A.~Mader, und F.W.~Vaandrager, "Operational and Logical Semantics for Polling RealTime Systems,".
@TECHREPORT{DFMV98full,
author = {H.~Dierks and A.~Fehnker and A.~Mader and F.W.~Vaandrager},
title = {{Operational and Logical Semantics for Polling RealTime Systems}},
institution = {Computer Science Institute Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen},
year = {1998},
number = {CSIR9813},
month = APR, optnote = {full paper of \cite{DFMV98}} } 
[inproceedings] bibtexH.~Dierks und J.~Tapken, "ToolSupported Hierarchical Design of Distributed RealTime Systems, pp. 222229.
@INPROCEEDINGS{DT98,
author = {H.~Dierks and J.~Tapken},
title = {{ToolSupported Hierarchical Design of Distributed RealTime Systems}},
booktitle = {Proceedings of the 10th EuroMicro Workshop on Real Time Systems},
year = {1998},
pages = {222229},
month = JUN, publisher = {IEEE Computer Society} } 
[techreport] bibtexK. Feyerabend, "Real time symbolic timing diagrams,".
@TECHREPORT{feyerabend96b,
author = {Konrad Feyerabend},
title = {Real time symbolic timing diagrams},
institution = {Department of computer science, Oldenburg University},
year = {1996},
month = Sep, note = {http://ca.informatik.unioldenburg.de},
abstract = {Symbolic Timing Diagrams have been introduced to increase acceptance of formal specification methods among hardware designers. Within the FORMAT project they have been used as input language to automated verification tools. They have proven to be very valuable for easy to understand specifications of critical system requirements. Over the past few years, quantitative (real time) timing aspects have gained increasing attendance in formal specification and verification. Intuitively, adding real time requirements to the graphical denotation of symbolic timing diagrams is easily accomplished by annotating constraint arcs to carry time intervals. In this paper we define the formal semantics of real time timing diagrams by a translation to timed propositional temporal logic. It is intended as technical reference and assumes some knowledge on STD. For an introduction to real time symbolic timing diagrams refer to Feyerabend/Josko: Graphical Specification with Real Time Symbolic Timing Diagrams.},
postscript = {feyerabend96b.ps} } 
[inproceedings] bibtexK. Feyerabend und B. Josko, "A Visual Formalism for Real Time Requirement Specifications, pp. 156168.
@INPROCEEDINGS{feyerabend96c,
author = {Konrad Feyerabend and Bernhard Josko},
title = {A Visual Formalism for Real Time Requirement Specifications},
booktitle = {TransformationBased Reactive Systems Development, Proceedings, 4th International {AMAST} Workshop on RealTime Systems and Concurrentand Distributed Software, {ARTS'97}},
year = {1997},
editor = {Miquel Bertran and Teodor Rus},
series = {Lecture Notes in Computer Science 1231},
pages = {156168},
publisher = {SpringerVerlag},
abstract = {This paper presents a semantical basis of a graphical specification language, called {\em realtime symbolic timing diagrams (RTSTD)},
to express realtime requirements of embedded systems. RTSTD allow a concise and unambigous formulation of realtime properties that are intuitively understandable by hardware designers. We give a precise semantical foundation of this graphical language in terms of realtime temporal logic. Due to this interpretation RTSTD can be embedded into existing verification tools to check whether an implementation satiesfies the given specification expressed as RTSTD.},
postscript = {feyerabend96c.ps} } 
[inproceedings] bibtexK. Feyerabend und R. Schlör, "Hardware Synthesis from Requirement Specifications.
@INPROCEEDINGS{Feyerabend:Schloer:1996,
author = {Konrad Feyerabend and Rainer Schl{\"o}r},
title = {Hardware Synthesis from Requirement Specifications},
booktitle = {EURODAC'96 with EUROVHDL'96 Proceedings},
year = {1996},
month = {September},
publisher = {IEEE Computer Society Press},
abstract = {This paper describes the theory and implementation of a novel system for hardware synthesis from requirement specifications expressed in a graphical specification language called Symbolic Timing Diagrams (STD). The system can be used together with an existing formalverification environment for VHDL leading to a novel methodology based on the combination of synthesis and formal verification. We show the feasibility of the approach and experimental results obtained with the system on the well known example of an industrial production cell, where both FPGA and ASIC hardware implementations were successfully synthesized.},
postscript = {feyerabend96a.ps} } 
[inproceedings] bibtexM. Fränzle, "Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, pp. 126140.
@INPROCEEDINGS{fraenzle99a,
author = {Fr{\"a}nzle, Martin},
title = {Analysis of Hybrid Systems: An ounce of realism can save an infinity of states},
booktitle = {Computer Science Logic (CSL'99)},
year = {1999},
editor = {Flum, J{\"o}rg and Rodr{\'\i}guezArtalejo, Mario},
volume = {1683},
series = {Lecture Notes in Computer Science},
pages = {126140},
publisher = {Springer Verlag},
abstract = {Hybrid automata have been introduced in both control engineering and computer science as a formal model for the dynamics of hybrid discretecontinuous systems. In the case of socalled linear hybrid automata this formalization supports semidecision procedures for state reachability, yet no decision procedures due to inherent undecidability. Thus, unlike finite or timed automata, already linear hybrid automata are outofscope of fully automatic verification. In this article, we devise a new semidecision method for safety of linear and polynomial hybrid systems which may only fail on pathological, practically uninteresting cases. These remaining cases are such that their safety depends on the {\em complete} absence of noise, a situation unlikely to occur in real hybrid systems. Furthermore, we show that if low probability effects of noise are ignored akin to the way they are suppressed in digital modelling then safety becomes fully decidable.},
postscript = {fraenzle99a.ps} } 
[unpublished] bibtexModelChecking DenseTime Duration Calculus.
@UNPUBLISHED{fraenzle98b,
author = {Fr{\"a}nzle, Martin},
title = {ModelChecking DenseTime Duration Calculus},
note = {Presented at the Duration Calculus Track of the 33rd European Summer School on Logic, Language and Information (an extended version has been submitted for a special issue of BCS FACS, to appear in 2001)},
month = aug, year = {1998},
abstract = {Since the seminal work of Zhou Chaochen, M.\,R.~Hansen, and P.~Sestoft on decidability of Duration Calculus it is wellknown that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that keypress verification with respect to elaborate DC specifications were impossible, we show that modelchecking {\em realistic} designs is nevertheless feasible. The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of embedded realtime systems. By analyzing two suitably sparser model classes we obtain modelchecking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.},
postscript = {fraenzle98b.ps} } 
[inproceedings] bibtexM. Fränzle, W. Goerigk, B. von Karger, und M. MüllerOlm, "Beyond ProCoS at Kiel: A Synopsis of Recent Research, pp. 117.
@INPROCEEDINGS{FraenzleEA:BeyondProCoSKiel,
author = {Fr{\"a}nzle, Martin and Goerigk, Wolfgang and Karger, Burghard von and M{\"u}llerOlm, Markus},
title = {Beyond {ProCoS} at {Kiel}: A Synopsis of Recent Research},
booktitle = {ProCoS WG Workshop at FM'99 (Part of the FM'99 CDRom)},
year = {1999},
pages = {117},
month = {September},
publisher = {Springer electronic media},
abstract = {This article presents an overview over research activities at various German universities which were sparked by the broad scope of topics covered by the Kiel ProCoS group.},
postscript = {fraenzle99b.ps} } 
[inproceedings] bibtexM. Fränzle und K. Lüth, "Visual Temporal Logic as a Rapid Prototyping Tool, pp. 115.
@INPROCEEDINGS{FraenzleLueth:VisualTLasRPTool,
author = {Fr{\"a}nzle, Martin and L{\"u}th, Karsten},
title = {Visual Temporal Logic as a Rapid Prototyping Tool},
booktitle = {Proc. 1st internat. Symp. on Visual Formal Methods (VFM `99)},
year = {1999},
editor = {D. Bosnacki, S. Mauw, T. Willemse},
number = {9908},
series = {Computer Science Reports},
pages = {115},
publisher = {Eindhoven University of Technology},
annote = {An extended version has appeared in Computer Languages 27(13), p. 93113} } 
[inproceedings] bibtexM. Fränzle und K. Lüth, "Compiling Graphical RealTime Specifications into Silicon.
@INPROCEEDINGS{fraenzle98a,
author = {Fr{\"a}nzle, Martin and L{\"u}th, Karsten},
title = {Compiling Graphical RealTime Specifications into Silicon},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'98)},
year = {1998},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
abstract = {Two different approaches towards automatic synthesis of embedded controllers from fully formal graphical specifications are presented. The source language is {\em realtime symbolic timing diagrams},
which are a {\em metrictime temporal logic} s.t.\ hard realtime constraints have to be dealt with. In the first synthesis method, we use a classical approach with first order temporal logic and B\"uchi automata as intermediate representations. As this leads to state explosion and unsatisfactory circuit complexity when largescale timing constraints are encountered, a second, novel technique is currently under development. Here, timed automata are used as intermediate representation, and timing constraints, if found to be sufficiently independent, are directly mapped to hardware timers.},
postscript = {fraenzle98a.ps} } 
[inproceedings] bibtexM. Fränzle und M. MüllerOlm, "Compilation and Synthesis for RealTime Embedded Controllers, pp. 256287.
@INPROCEEDINGS{fraenzle99c,
author = {Fr{\"a}nzle, Martin and M{\"u}llerOlm, Markus},
title = {Compilation and Synthesis for RealTime Embedded Controllers},
booktitle = {Correct System Design  Recent Insights and Advances},
year = {1999},
editor = {Olderog, ErnstR{\"u}diger and Steffen, Bernhard},
volume = {1710},
series = {Lecture Notes in Computer Science},
pages = {256287},
publisher = {Springer Verlag},
abstract = {This article provides an overview over two constructive approaches to provably correct hard realtime code generation where hard realtime code is \emph{generated} from abstract requirements rather than \emph{verified} against the timing requirements \emph{a posteriori}. The first, more pragmatic approach is concerned with translation of imperative programs, extended by hard realtime commands which allow one to specify upper bounds for the execution time of basic blocks. In the second approach, Duration Calculus, a metrictime temporal logic, is used as the source language. Duration Calculus allows one to specify realtime systems at a very high level of abstraction.},
postscript = {fraenzle99c.ps} } 
[inproceedings] bibtexM. Grabowski und H. Hungar, "On the existence of effective Hoare logics, pp. 428435.
@INPROCEEDINGS{hungar:GrHu88,
author = {Michal Grabowski and Hardi Hungar},
title = {On the existence of effective {H}oare logics},
booktitle = {3rd IEEE Symp.\ on Logic in Comp.\ Sc.},
year = {1988},
pages = {428435},
key = {GrHu88} } 
[inproceedings] bibtexH. Hungar, "Correctness of programs over poor signatures, pp. 109120.
@INPROCEEDINGS{hungar:Hun91c,
author = {Hardi Hungar},
title = {Correctness of programs over poor signatures},
booktitle = {Foundations of Software Technology and Theoretical Comp.\ Sc.},
year = {1991},
editor = {S. Biswas and K. V. Nori},
series = {LNCS 560},
pages = {109120},
key = {Hun91c} } 
[incollection] bibtexH. Hungar, "Specification and Verification Using a Visual Formalism on Top of Temporal Logic, Broy, M., Merz, S., und Spies, K., Eds., pp. 305339.
@INCOLLECTION{hungar:Hun96e,
author = {H. Hungar},
title = {Specification and Verification Using a Visual Formalism on Top of Temporal Logic},
booktitle = {Formal Systems Specification: The RPCMemory Specification Case Study},
publisher = {Springer},
year = {1996},
editor = {Manfred Broy and Stephan Merz and Katharina Spies},
series = {LNCS 1169},
pages = {305339},
key = {Hun96e} } 
[inproceedings] bibtexH. Hungar, "Combining model checking and theorem proving to verify parallel processes, pp. 154165.
@INPROCEEDINGS{hungar:Hun93b,
author = {H. Hungar},
title = {Combining model checking and theorem proving to verify parallel processes},
booktitle = {5th Int.\ Conf.\ on Computer Aided Verification},
year = {1993},
editor = {C. Courcoubetis},
series = {LNCS 697},
pages = {154165},
publisher = {Springer},
key = {Hun93b} } 
[inproceedings] bibtexH. Hungar, "Model checking of macro processes, pp. 169181.
@INPROCEEDINGS{hungar:Hun94a,
author = {H. Hungar},
title = {Model checking of macro processes},
booktitle = {6th Int.\ Conf.\ on Computer Aided Verification},
year = {1994},
editor = {D.L. Dill},
series = {LNCS 818},
pages = {169181},
publisher = {Springer},
key = {Hun94a} } 
[inproceedings] bibtexH. Hungar, "The complexity of verifying functional programs, pp. 428439.
@INPROCEEDINGS{hungar:Hun93a,
author = {H. Hungar},
title = {The complexity of verifying functional programs},
booktitle = {Symp.\ on Theoretical Aspects of Comp.\ Sc.},
year = {1993},
editor = {P. Enjalbert and A. Finkel and K.W. Wagner},
series = {LNCS 665},
pages = {428439},
publisher = {Springer},
key = {Hun93a} } 
[inproceedings] bibtexH. Hungar, "Complexity of proving program correctness, pp. 459474.
@INPROCEEDINGS{hungar:Hun91b,
author = {Hardi Hungar},
title = {Complexity of proving program correctness},
booktitle = {Theoretical Aspects of Computer Software},
year = {1991},
editor = {T. Ito and A. R. Meyer},
series = {LNCS 526},
pages = {459474} } 
[inproceedings] bibtexH. Hungar, "Local model checking for parallel compositions of contextfree processes, pp. 114128.
@INPROCEEDINGS{hungar:Hun94b,
author = {H. Hungar},
title = {Local model checking for parallel compositions of contextfree processes},
booktitle = {5th Int.\ Conf.\ on Concurrency Theory},
year = {1994},
editor = {B. Jonsson and J. Parrow},
series = {LNCS 836},
pages = {114128},
publisher = {Springer},
key = {Hun94b} } 
[inproceedings] bibtexH. Hungar, "Model Checking and HigherOrder Recursion, pp. 149159.
@INPROCEEDINGS{hungar99MFCS,
author = {Hardi Hungar},
title = {Model Checking and HigherOrder Recursion},
booktitle = {Math.\ Found.\ of Comp.\ Sc.},
year = {1999},
editor = {Miros{\l}aw Kuty{\l}owski and Leszek Pacholski and Thomasz Wierzbicki},
series = {LNCS 1672},
pages = {149159},
publisher = {Springer},
abstract = {Since Muller and Schupp have shown in 1985 that monadic secondorder logic (MSOL) is decidable for contextfree graphs, several specialized procedures have been developed for related problems, mostly for sublogics like the modal mucalculus, or even its alternationfree fragment. This work shows the decidability of S1S, the trace version of MSOL, for the richer set of \emph{macro graphs}. The generation mechanism of macro graphs is of higherorder nature and relates to the contextfree one like macro grammars [Fischer, 1968] relate to contextfree grammars. Technically, the result follows from the decidability of the emptiness problem of the trace language of a macro graph with fairness. The decision procedure is given in form of a tableau system. Soundness and completeness follow from the relation of the (finite) tableaux to their infinite unfoldings. This kind of proof promises to be helpful in the derivation of further results.},
postscript = {hungar99MFCS.ps} } 
[article] bibtexH. Hungar, "Expressibility of the semantics of sequential programs in firstorder logic, pp. 345366
@ARTICLE{hungar:Hun94d,
author = {Hardi Hungar},
title = {Expressibility of the semantics of sequential programs in firstorder logic},
journal = {Fundamenta Informatica},
year = {1994},
volume = {21},
pages = {345366},
key = {Hun94d} } 
[inproceedings] bibtexH. Hungar, "Complexity bounds of Hoarestyle proof systems, pp. 120126.
@INPROCEEDINGS{hungar:Hun91a,
author = {Hardi Hungar},
title = {Complexity bounds of Hoarestyle proof systems},
booktitle = {6th IEEE Symp.\ on Logic in Comp.\ Sc.},
year = {1991},
pages = {120126},
key = {Hun91a} } 
[inproceedings] bibtexH. Hungar, O. Grumberg, und W. Damm, "What if model checking must be truly symbolic, pp. 120.
@INPROCEEDINGS{hungar:HGD95,
author = {H. Hungar and O. Grumberg and W. Damm},
title = {What if model checking must be truly symbolic},
booktitle = {Work.\ Conf.\ on Correct Hardware Design and Verification Methods},
year = {1995},
editor = {P. Camurati and H. Eveking},
series = {LNCS 987},
pages = {120},
publisher = {Springer},
key = {HGD95} } 
[inproceedings] bibtexH. Hungar und B. Steffen, "Local model checking for contextfree processes, pp. 593605.
@INPROCEEDINGS{hungar:HuSt93,
author = {H. Hungar and B. Steffen},
title = {Local model checking for contextfree processes},
booktitle = {20th Int.\ Coll.\ on Automata, Languages and Programming},
year = {1993},
editor = {A. Lingas and R. Karlsson and S. Carlsson},
series = {LNCS 700},
pages = {593605},
publisher = {Springer},
key = {HuSt93} } 
[article] bibtexH. Hungar und B. Steffen, "Local model checking for contextfree processes, pp. 364385
@ARTICLE{hungar:HuSt94,
author = {H. Hungar and B. Steffen},
title = {Local model checking for contextfree processes},
journal = {Nordic J.\ of Comp.},
year = {1994},
volume = {1},
pages = {364385},
key = {HuSt94} } 
[inproceedings] bibtexB. Josko, "Verifying the correctness of AADL modules using model checking, pp. 386400.
@INPROCEEDINGS{josko90a,
author = {Bernhard Josko},
title = {Verifying the correctness of {AADL} modules using model checking},
booktitle = {Stepwise Refinement of Distributed Systems. {Models, Formalisms, Correctness}},
year = {1990},
editor = {Jaco W. de Bakker and WillemPaul de Roever and Grzegorz Rozenberg},
series = {Lecture Notes in Computer 430},
pages = {386400},
publisher = {SpringerVerlag},
abstract = {This paper presents a temporal logic MCTL which is suitable for modular specification and verification of computer architectures. MCTL has the advantage that open systems can be specified and verified; i.e.\ it allows the specification of properties under some assumptions on the environment. The module concept may help to solve the state explosion problem in the verification of temporal logic specifications. To verify the correctness of an implementation we describe a model checking algorithm for that logic. } } 
[inproceedings] bibtexB. Josko, "Context Dependent Bisimulation, pp. 155160.
@INPROCEEDINGS{josko91c,
author = {Bernhard Josko},
title = {Context Dependent Bisimulation},
booktitle = {Proceedings of the 3rd Workshop on Concurrency and Compositionality},
year = {1991},
editor = {Eike Best and Grzegorz Rozenberg},
series = {{GMD}Studien Nr. 191},
pages = {155160},
abstract = {Bisimulation is used to describe the behavioural equivalence of labelled transition systems. In [Brown, Clarke, Grumberg 1988] an analogue definition is given for state based systems (Kripke structures) and it is shown that the notion of bisimulation coincides with the equivalence induced by the temporal logic CTL*. We will generalize their results concerning weak bisimulation to reactive systems. A reactive system is an open system interacting with its environment, and consequently its behaviour depends on the actions of the environment. Hence an equivalence relation for reactive systems should include the reactions of the environment. This leads to a notion of relativized bisimulation. For action based systems such a context dependent bisimulation is given in [Larsen 1987], where the environment constraints are given by an action system too. We define a relativized (weak) bisimulation for Kripke structures where the environment constraints are given by a temporal logic specification. We show that this notion of relativized bisimulation coincides with the relativized equivalence induced by the temporal logic CTL* without the nexttimeoperator. Furthermore, we show that it is possible to construct a CTL formula which uniquely characterizes a Kripke structure relatively to a given environment. } } 
[inproceedings] bibtexB. Josko, "A Context Dependent Equivalence Relation between Kripke structures, pp. 341358.
@INPROCEEDINGS{josko91a,
author = {Bernhard Josko},
title = {A Context Dependent Equivalence Relation between {K}ripke structures},
booktitle = {ComputerAided Verification '90},
year = {1991},
editor = {E. M. Clarke and R. P. Kurshan},
series = {{DIMACS} Series in Discrete Mathematics and Theoretical Computer Science, Volume 3},
pages = {341358},
publisher = {American Mathematical Society},
abstract = {In [BCG87] Browne, Clarke and Grumberg define a bisimulation relation on Kripke structure and give a characterization of this equivalence relation in temporal logic. We will generalize their results to reactive systems, which are modelled by Kripke structures together with some constraints describing some requirements how the environment has to interact with the module. Our results subsume the result of [BCG87] by using the constraint {\em true}. Furthermore, it answers the questions raised in that paper how the equivalence of Kripke structures with fairness constraints can be characterized.} } 
[inproceedings] bibtexB. Josko, "A Context Dependent Equivalence Relation between Kripke structures. (Extended Abstract), pp. 204213.
@INPROCEEDINGS{josko91b,
author = {Bernhard Josko},
title = {A Context Dependent Equivalence Relation between {K}ripke structures. (Extended Abstract)},
booktitle = {ComputerAided Verification 1990, Proceedings},
year = {1991},
editor = {E. M. Clarke and R. P. Kurshan},
series = {Lecture Notes in Computer Science 531},
pages = {204213},
publisher = {SpringerVerlag},
abstract = {In [BCG88] Browne, Clarke and Grumberg define a bisimulation relation on Kripke structure and give a characterization of this equivalence relation in temporal logic. We will generalize their results to reactive systems, which are modelled by Kripke structures together with some constraints describing some requirements how the environment has to interact with the module. Our results subsume the result of [BCG88] by using the constraint {\em true}. Furthermore, it answers the questions raised in that paper how the equivalence of Kripke structures with fairness constraints can be characterized. } } 
[inproceedings] bibtexB. Josko, "Modelchecking of CTL Formulae under Liveness Assumptions, pp. 280289.
@INPROCEEDINGS{josko87,
author = {Bernhard Josko},
title = {Modelchecking of {CTL} Formulae under Liveness Assumptions},
booktitle = {{ICALP} 87},
year = {1987},
editor = {Th. Ottmann},
series = {Lecture Notes in Computer 267},
pages = {280289},
publisher = {SpringerVerlag},
abstract = {Our aim is a modular verification method for concurrent systems. To verify a module separated from the other components we have to assume some (correct) behaviour of these components concerning the interactions with the module under consideration. These reactions of the other modules can be described by liveness properties. Hence in a modular verification method we have to prove a formula under some liveness assumptions. A logic which is able to express the correctness of a subsystem under some liveness assumption is e.g.\ CTL* or only its linear time part TL. But model checking for CTL* is exponential in the size of a given formula. Hence, often CTL is used instead of CTL* in specifications of concurrent systems as this logic has a linear model checking algorithm. But CTL has a restricted expressive power, e.g.\ it is not expressible that some property holds under some liveness assumptions. In this paper we define a logic LCTL, which is an extension of CTL where quantifications over paths are interpreted with respect to some liveness assumptions.I.e., formulae of LCTL are pairs $(l,f)$ where $l$ is a liveness assumption (expressed in TL) and $f$ is a CTL formula. } } 
[phdthesis] bibtexB. Josko, "Modular Specification and Verification of Reactive Systems,".
@PHDTHESIS{josko93c,
author = {Bernhard Josko},
title = {Modular Specification and Verification of Reactive Systems},
school = {Universit\"at Oldenburg},
year = {1993},
type = {Habilitationsschrift},
abstract = {In this thesis we develop a theory for compositional verification of reactive systems in the framework of assumption/commitment style logic. Due to the fact that the state space of a system may grow exponentially with the number of its components (a phenomenon commonly referred to as the state explosion problem) modular and compositional verification methods are necessary to verify the correctness of large programs and systems. \parThe background of our work is twofold: On one hand it is based on temporal logic which is a comprehensive and well established specification language for expressing a wide spectrum of properties of reactive systems. On the other hand {\em assumption/commitment} style specifications have to be used to express the dependency of the behaviour of a system on the interaction with its environment; so the specification of a system is given always relatively to an expected behaviour of its environment. \par In this thesis we combine the theory of assumption/commitment specifications with the theory of {\em branching time} temporal logic and present the logic MCTL* as an extension of the branching time temporal logic CTL*. We develop a design methodology for compositional verification using assumption/commitment specifications of branching time temporal logic which subsumes the linear time approach. \par Our compositional approach overcomes the state explosion problem in a way that basic components of a complex system can be verified automatically using a special model checking algorithm. We present an efficient model checking algorithm for assumption/commitment specifications which is an extension of the wellknown CTL model checker. To verify complex systems proof rules are given to derive properties of the global systems from already established properties of its components. The presented proof calculus is complete for finite systems. The feasibility of our approach is demonstrated by typical examples. \par Theoretical explorations of the temporal logic MCTL* are given. We classify the logic MCTL* within the hierarchy of branching time temporal logics and show that MCTL* subsumes the logic CTL* and can be embedded into the $\mu$calculus of alternation depth 2. This embedding is achieved by means of a translation into ECTL, an automata extension of CTL*. Furthermore, a uniform semantics definition for CTL*, fair CTL*, MCTL* and others is given introducing the notion of extended computation trees. } } 
[inproceedings] bibtexJürgen Bohn, "Interaktive Synthese kommunizierender Systeme mit LAMBDA, pp. 116121.
@INPROCEEDINGS{Bohn93a,
author = {{J{\"u}rgen Bohn}},
title = {{I}nteraktive {S}ynthese kommunizierender {S}ysteme mit {LAMBDA}},
booktitle = {{GI/ITG} Workshop Formale Methoden zum Entwurf korrekter Systeme},
year = {1993},
editor = {{Th. Kropf} and {R. Kumar} and {D. Schmid}},
pages = {116121},
address = {Bad Herrenalb},
month = mar, organization = {GI/ITG},
publisher = {Universit{\"a}t Karlsruhe, Interner Bericht Nr. 10/93},
abstract = { },
postscript = {Bohn93a.ps.gz} } 
[inproceedings] bibtexJ. Klose, "Erweiterte Message Sequence Charts für die Verifikation von StatemateEntwürfen, pp. 181189.
@INPROCEEDINGS{klose99b,
author = {Jochen Klose},
title = {Erweiterte {M}essage {S}equence {C}harts f\"ur die {V}erifikation von {S}tatemate{E}ntw\"urfen},
booktitle = {Informatik'99  Informatik \"uberwindet Grenzen, 29. Jahrestagung der Gesellschaft f\"ur Informatik},
year = {1999},
editor = {K. Beiersd\"orfer and G. Engels and W. Sch\"afer},
pages = {181189},
publisher = {Springer Verlag},
abstract = {Das DFG Schwerpunktprogramm \"Integration von Techniken der Softwarespezifikation f\"ur ingenieurwissenschaftliche Anwendungen\" besch\"aftigt sich mit dem Zusammenspiel Beschreibungstechniken der Informatik und der Ingeniuerwissenschaften bei der Spezifikation von Software. Dieser Artikel stellt die Arbeiten des Einzelprojektes \"Usecase driven Specification of Engineering Applications\" vor. Es wird eine kurze Einführung in die Thematik des Schwerpunktprogramms gegeben, sowie das Vorgehen bei der Verifikation von StatemateEntw\"urfen erl\"autert. Es wird ebenfalls eine kurze Einf\"uhrung in den Industriestandard \"Message Sequence Charts\" gegeben, bevor die Erweiterungen dieses Standards vorgestellt werden.} } 
[inproceedings] bibtexF. Liu und T. Peikenkamp, "Evaluation and Parallelization of Functions in Functional Logic Languages.
@INPROCEEDINGS{LP92,
author = {F. Liu and T. Peikenkamp},
title = {Evaluation and Parallelization of Functions in Functional Logic Languages},
booktitle = {Proc. of the 4th International Workshop on the Parallel Implementation of Functional Languages},
year = {1992},
address = {Aachen, Germany},
month = {September} } 
[inproceedings] bibtexF. Liu, T. Peikenkamp, und W. Damm, "An extended gradient model for NUMA multiprocessors, pp. 210224.
@INPROCEEDINGS{liu95a,
author = {F. Liu and T. Peikenkamp and W. Damm},
title = {An extended gradient model for {NUMA} multiprocessors},
booktitle = {Algorithms, Concurrency and Knowledge, Proc.\ Asian Computing Science Conference},
year = {1995},
editor = {K. Kanchanasut and J.J. L{\'e}vy},
volume = {1023},
series = {Lecture Notes in Computer Science},
pages = {210224},
abstract = {In this paper, we present the design and implementation of an effective and scalable dynamic load balancing system for NonUniform Memory Access (NUMA) multiprocessors where load balancing is a key issue to achieve adequate efficiency. The proposed load balancing algorithm extends the wellknown gradient model to enhance its applicability in a wide range of multiprocessor systems and to improve the overall system performance. A comparative performance study between the two models based on the preliminary simulation results is also reported in the paper.},
postscript = {liu95a.ps} } 
[inproceedings] bibtexK. Lüth, "The ICOS Synthesis Environment, pp. 294297.
@INPROCEEDINGS{lueth98b,
author = {L{\"u}th, Karsten},
title = {The {ICOS} {S}ynthesis {E}nvironment},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems},
year = {1998},
editor = {Ravn, A.P. and Rischel, H.},
volume = {1486},
series = {LNCS},
pages = { 294297},
month = {September},
publisher = {Springer Verlag},
abstract = {This paper presents an overview of the ICOS system, a design environment for controldominated reactive systems, which is based on a graphical specification language called realtime symbolic timing diagrams. ICOS offers a broad set of tools to create, verify, and to synthesize hardware or software code from timing diagram specifications. },
postscript = {lueth98b.ps} } 
[conference] bibtexK. Lüth, "From RealTime Timing Diagrams to Silicon: Compiling RealTime R equirement Specifications, pp. 152159.
@CONFERENCE{lueth99a,
author = {Karsten L{\"u}th},
title = {From RealTime Timing Diagrams to Silicon: Compiling RealTime R equirement Specifications},
booktitle = {5th International Conference on Information Systems, Analysis an d Synthesis (ISAS'99 together with SCI'99)},
year = {1999},
editor = {Michel Torres and Belkis Sanchez and Addelaziz Bouras and Weimin g Shen},
pages = {152159},
month = {August},
organization = {International Institute of Informatics and Systemics together with IEEE},
abstract = {Formalized languages are now widely used to specify protocols for hardwarelike systems. In this article we present tools which generate executable code from requirements that are expressed in a formalized graphical realtime specification language, the socalled {\em Real Time Symbolic Timing Diagrams} (or RTSTD, for short). The first set of tools automatically derives a prototype implementation of the specified component,which is correct by construction in respect to the specification. The second set of tools produces executable code, which can be used during testing to check whether the component under test satisfies or violates the requirements. },
postscript = {lueth99a.ps} } 
[inproceedings] bibtexK. Lüth, A. Metzner, T. Peikenkamp, und J. Risau, "The EVENTS Approach to Rapid Prototyping for Embedded Control Systems, pp. 4554.
@INPROCEEDINGS{peikenkamp97a,
author = {K. L{\"u}th and A. Metzner and T. Peikenkamp and J. Risau},
title = {The {EVENTS} Approach to Rapid Prototyping for Embedded Control Systems},
booktitle = {Workshops zur Architektur von Rechensystemen:ARCS '97},
year = {1997},
editor = {R. Hoffmann and B. Klauer and Ch. M\"ullerSchloer and K.D. Reinatz and D. Tavangarian and K. Waldschmidt and H. Ch. Zeidler},
pages = {4554},
address = {Rostock, Germany},
month = sep, organization = {ITG and GI},
abstract = {This paper presents a prototyping system for embedded control applications (ECAs) which is currently being developed at the Computer Architecture group of the University of Oldenburg. Part of this system is a hardware architecture which acts as a target for prototyping and uses multithreaded processors to aim at those ECAs that require fast reaction to external events (i.e. sensor input). The other part consists of software tools that allow users to automatically generate code for this architecture using graphical specification languages.},
html = {http://ca.informatik.unioldenburg.de/publications/zes97/zes97.html},
postscript = {peikenkamp97a.ps} } 
[inproceedings] bibtexK. Lüth, J. Niehaus, und A. Metzner, "A Statematebased Rapid Prototyping Environment.
@INPROCEEDINGS{lueth98c,
author = {L{\"u}th, Karsten and Niehaus, J{\"ur}gen and Metzner, Alexander},
title = {A Statematebased Rapid Prototyping Environment},
booktitle = {6. {D}eutsches {A}nwenderforum f{\"ur} Statemate},
year = {1998},
month = may, abstract = {This paper presents a rapid prototyping environment for hardware/software codesign of embedded control applications in which Statemate is used as specification and codesynthesis tool. The environment, which is currently being developed at the Computer Architecture Group of the University of Oldenburg, consists of a programmable FPGA field, processor boards, and a programming environment which automates all synthesis steps from the initial Statemate model down to executable hardware and software code. },
postscript = {lueth98c.ps} } 
[inproceedings] bibtexK. Lüth, . Peikenkamp, und J. Niehaus, "HW/SW Cosynthesis using Statecharts and Symbolic Timing Diagrams.
@INPROCEEDINGS{lueth98a,
author = {L{\"u}th, Karsten and Peikenkamp, {T}homas and Niehaus, J{\"u}rgen},
title = {{HW/SW} {C}osynthesis using {S}tatecharts and {S}ymbolic {T}iming {D}iagrams},
booktitle = {Proceedings of the 9th {IEEE} International Workshop on {R}apid {S}ystem {P}rototyping},
year = {1998},
month = {Juni},
abstract = {This paper presents a hardware/software cosynthesis environment for embedded systems which is currently being developed at the Computer Architecture Group of the University of Oldenburg. We use two graphical formalisms as specification languages and synthesize code for a multiprocessor rapid prototyping board. The two major problems we deal with are first, to realize an efficient distributed execution of the specified system and second, to develop automated interfacecode generation for the hardware and software parts of the system under design.},
postscript = {lueth98a.ps} } 
[inproceedings] bibtexA. Lüdtke, "Abstraktionsbasierte Erklärungen für Prognose und Diagnose mit BayesNetzen.
@INPROCEEDINGS{Luedtke1997a,
author = {Lüdtke, A.},
title = {{Abstraktionsbasierte Erklärungen für Prognose und Diagnose mit BayesNetzen}},
booktitle = {{Beiträge zum 8. Arbeitstreffen der GIFachgruppe 1.1.5/7.0.1 "`Intelligente Lehrund Lehrsysteme"', Duisburg, 18.19. September 1997, "`Blaue Berichte"' der TU München}},
year = {1997},
editor = {C. Herzog},
series = {Blaue Berichte},
publisher = {TU München},
owner = {luedtke},
timestamp = {2006.10.13} } 
[techreport] bibtexA. Lüdtke, "Intervention bei Sorglosigkeit in der Sicherheitsanalyse. Abschlußbericht des Projektes SUCCESS (Support for Safety Critical Complex Embedded Systems,".
@TECHREPORT{Luedtke1999,
author = {Lüdtke, A.},
title = {{Intervention bei Sorglosigkeit in der Sicherheitsanalyse. Abschlußbericht des Projektes SUCCESS (Support for Safety Critical Complex Embedded Systems}},
institution = {{Oldenburger Forschungs und Entwicklungsinstitut für InformatikWerkzeuge und Systeme, Forschungsbereich Eingebettete Systeme}},
year = {1999},
owner = {luedtke},
timestamp = {2006.12.13} } 
[book] bibtexA. Lüdtke, Abstraktionsbasierte Erklärungen für Wahrscheinlichkeitsberechnungen mit BayesNetzen
@BOOK{Luedtke1997, title = {Abstraktionsbasierte Erklärungen für Wahrscheinlichkeitsberechnungen mit BayesNetzen},
publisher = {{Carl von Ossietzky Universität Oldenburg, Fachbereich Informatik, Ammerländer Heerstraße 114118, 26129 Oldenburg, Deutschland}},
year = {1997},
author = {Lüdtke, A.},
owner = {luedtke},
timestamp = {2006.12.13} } 
[article] bibtexA. Mikschl und W. Damm, "MSparc: A Multithreaded Sparc
@ARTICLE{mikschl96a,
author = {A. Mikschl and W. Damm},
title = {MSparc: A Multithreaded Sparc},
journal = {Lecture Notes on Computer Science},
year = {1996},
abstract = {This paper presents a multithreaded processor, the MSparc. MSparc supports up to four contexts on chip and employs block multithreading. The processor is compatible to standard Sparc processors making multithreading completely transparent to application programs. Switching can be done by hardware or software and is achieved within one processor cycle. Preliminary performance evaluations in a NUMA architecture with weak cache coherence show processor utilization of up to 83\%.},
postscript = {mikschl96a.ps} } 
[techreport] bibtexC. Möbus und A. Lüdtke, "Eingebettete Systeme: Wissensakquisition für die Risikoanalyse.,".
@TECHREPORT{MoebusLuedtke1999,
author = {M{\"o}bus, C. and L{\"u}dtke, A.},
title = {{Eingebettete Systeme: Wissensakquisition für die Risikoanalyse.}},
institution = {{Oldenburger Forschungs und Entwicklungsinstitut für InformatikWerkzeuge und Systeme, Jahresbericht 1998}},
year = {1999},
owner = {luedtke},
pages = {4244},
timestamp = {2006.12.13} } 
[inproceedings] bibtexJ. R. (. Niehaus), A. Mikschl, und W. Damm, "A RISC Approach to Weak Cache Coherence, pp. 453456.
@INPROCEEDINGS{risau96a,
author = {J\"urgen Risau (now: Niehaus) and Alfred Mikschl and Werner Damm},
title = {A {RISC} Approach to Weak Cache Coherence},
booktitle = {EuroPar'96 Parallel Processing: Second International EuroPar Conference, Vol. II},
year = {1996},
editor = {Luc Bouge and Pierre Fraigniaud and Anne Mignotte and Yves Robert},
series = {LNCS 1124},
pages = {453456},
organization = {Springer Verlag},
abstract = {Data used by parallel programs can be divided into classes, based on how threads access it. For different classes of data different coherence mechanisms might be optimal. This paper presents four primitives designed for use in a shared memory multiprocessor system, where each processor has its private cache. Using these primitives, programmers can implement those coherence models that are best suited to their applications. The paper gives a description of the primitives and some implementation details. },
postscript = {risau96a.ps} } 
[techreport] bibtexJ. R. (. Niehaus), A. Mikschl, und W. Damm, "Implementation of a New Weak Cache Coherence Protocol,".
@TECHREPORT{risau96b,
author = {J\"urgen Risau (now: Niehaus) and Alfred Mikschl and Werner Damm},
title = {Implementation of a New Weak Cache Coherence Protocol},
institution = {CvO University of Oldenburg},
year = {1996},
abstract = { Most strong cache coherence protocols provide a sequential consistent memory model. Weak coherence models often give an, albeit restricted, view of this model, too. However, there are many different possibilities to write parallel programs and not all of them are based on sequential consistency. This paper presents a new cache coherence protocol that provides many different ways of implementing coherence and synchronization. Using this protocol threads can exploit knowledge about how they use data and decide which coherence scheme to use. An implementation of the protocol in a NUMA environment is described in detail and discussed. This is a long version of "A RISC Approach to Weak Cache Coherence" by the same authors.},
postscript = {risau96b.ps} } 
[techreport] bibtexJ. R. (. Niehaus), A. Stermann, und W. Damm, "Software Controlled Cache Coherence in SharedMemory Multiprocessors,".
@TECHREPORT{risau96c,
author = {J\"urgen Risau (now: Niehaus) and Astrid Stermann and Werner Damm},
title = {Software Controlled Cache Coherence in SharedMemory Multiprocessors},
institution = {CvO University of Oldenburg},
year = {1996},
abstract = { During the last few years many different memory consistency protocols have been proposed. These range from strong models like sequential consistency or processor consistency to weak ones like weak ordering, release consistency and SCNF. Implementations of these protocols are usually transparent to application programs: They try to hide as much detail as possible, usually leaving 'well behaved' applications with a sequential consistent memory view. There are two reasons why a different approach to memory consistency is chosen in this paper. On one hand this transparency of protocols imposes a limit on the amount of information about data access categories that can be given by applications. More information could reduce coherence overhead substantially. On the other hand sequential consistency is not the only feasible programming model for writing parallel programs. Most applications do not rely on the strong limitations given by it, because they synchronize to access shared data. We therefore propose processor primitives that allow applications to implement different consistency schemes for accesses to different data objects. We also describe the implementation of these primitives in a busbased shared memory NUMAArchitecture. To show the feasibility of such an architecture, preliminary performance results using orparallel Prolog programs are given.},
postscript = {risau96c.ps} } 
[inproceedings] bibtexR. Schlör, "A Prover for VHDLbased Hardware Design, pp. 643650.
@INPROCEEDINGS{Schloer95,
author = {R. Schl{\"o}r},
title = {A {P}rover for {VHDL}based {H}ardware {D}esign},
booktitle = {{IFIP} International Conference on Computer Hardware Description Languages and their Applications},
year = {1995},
pages = {643650},
month = {September},
abstract = {This paper gives a survey over a selfcontained part of the ESPRITproject ``FORMAT'', which developes a {\em prover} for VHDLbased hardware design. Notable is the use of a {\em graphical} specification language called STD , which can be seen as a visual dialect of temporal logic. The heart of the prover is built by two powerful industrial verification tools: A (compositional) symbolic model checker (developed by SIEMENS), and the LAMBDAtheorem prover (developed by AHL). The aim of this paper is to describe (1) the various tools integrated in the prover, (2) the graphical specification language STD with its associated design methodology, and (3) to explain how proofs about {\em generic} (parameterized) designs are performed in the prover, using a combination of automatic and interactive reasoning.},
postscript = {Schloer95.ps} } 
[inproceedings] bibtexR. Schlör, A. Allara, und S. Comai, "System Verification using UserFriendly Interfaces, pp. 167172.
@INPROCEEDINGS{SchloerAllaraComai99,
author = {R. Schl{\"o}r and A. Allara and S. Comai},
title = {{S}ystem {V}erification using {U}ser{F}riendly {I}nterfaces},
booktitle = {Design, Automation and Test in Europe / User Forum},
year = {1999},
pages = {167172},
publisher = {IEEE Computer Society Press},
abstract = {This paper reports on the use of a verification environment for VHDL based on automatic verification techniques 1. The paper focuses on two different aspects: (1) A graphical language and interface for the specification of properties called STDx (extended Symbolic Timing Diagrams) is described and its application is illustrated. (2) A methodology for formal verification of system properties based on a combination of modelchecking and tautologychecking is suggested.  A first account of successful application of the techniques on a selected industrial design is given.},
postscript = {SchloerAllaraComai99.ps} } 
[inproceedings] bibtexR. Schlör und W. Damm, "Specification and Verification of SystemLevel Hardware Designs using Timing Diagrams, pp. 518524.
@INPROCEEDINGS{SchloerDamm93,
author = {R. Schl{\"o}r and W. Damm},
title = {Specification and Verification of SystemLevel Hardware Designs using Timing Diagrams},
booktitle = {Proceedings, The European Conference onDesign Automation},
year = {1993},
pages = {518524},
address = {Paris, France},
publisher = {IEEE Computer Society Press},
abstract = {In this paper we present a novel approach to the specification and verification of systemlevel hardware designs. It is based on Timing Diagrams, a graphical specification language with an intuitive semantics, which is especially appropriate for the description of asynchronous distributed systems such as hardware designs. Timing Diagrams and their semantics are formally defined based on a translation to Temporal Logic. It is shown that for the resulting type of formulas there is an efficient modelchecking procedure, thus allowing fully automatic verification of hardware designs.},
postscript = {SchloerDamm93.ps} } 
[inproceedings] bibtexR. Schlör, B. Josko, und D. Werth, "Using a visual formalism for design verification in industrial environments, pp. 208221.
@INPROCEEDINGS{SchloerJoskoWerth98,
author = {R. Schl{\"o}r and B. Josko and D. Werth},
title = {Using a visual formalism for design verification in industrial environments},
booktitle = {VISUAL'98},
year = {1998},
series = {Lecture Notes in Computer Science 1385},
pages = {208221},
publisher = {SpringerVerlag},
abstract = { This paper reports experiences and results gained during the evaluation of the visual formalism {\em STD} as specification method for formal verification, performed in cooperation with industrial partners. The visual formalism {\em STD} ({\em S}ymbolic {\em T}iming {\em D}iagrams) was developed continuously since 1993 by OFFIS as a specification method, which satisfies several needs: (1) It is based on the principles used in the familiar notation of timing diagrams (as conventionally used by hardware designers). (2) It is a method amenable to formal verification, using stateofthe art verification tools efficiently (in particular, symbolic modelchecking). (3) It supports {\em compositional} verification, which is an approach to verify large designs in a compositional way (breaking up proofs of requirements stated for a full design into a sequence of smaller proof tasks, which imply the global proof task). The formalism (with the supporting tools) has been integrated into an established verification environment ({\em CheckOffM}), which allows to verify industrialscale designs by modelchecking.},
postscript = {SchloerJoskoWerth98.ps.gz} } 
[inproceedings] bibtexG. Schumacher, B. Josko, G. Wagner, und M. Radetzki, "Development of a Telephone Answering Machine in a Lab  FPGAs in Education, pp. 400404.
@INPROCEEDINGS{josko96,
author = {Guido Schumacher and Bernhard Josko and Gerhard Wagner and Martin Radetzki},
title = {Development of a Telephone Answering Machine in a Lab  {FPGAs} in Education},
booktitle = {Sixth International Workshop on Field Programmable Logic and Applications, {FPL'96}},
year = {1996},
series = {Lecture Notes in Computer Science 1142},
pages = {400404},
publisher = {SpringerVerlag},
abstract = {Practical experiences with stateoftheart synthesis and simulation tools are fundamental in the education of hardware designers. To understand the difficulties and problems in IC design, students should train each step in a design flow including the test of the completed system. We present our experience obtained in a one term lab using FPGAs as target technology. } } 
[phdthesis] bibtexG. Wittich, "Ein problemorientierter Ansatz zum Nachweis von Realzeiteigenschaften eingebetteter Systeme,".
@PHDTHESIS{wittich99a,
author = {Gunnar Wittich},
title = {Ein problemorientierter Ansatz zum Nachweis von Realzeiteigenschaften eingebetteter Systeme},
school = {CarlvonOssietzky Universit\"at Oldenburg},
year = {1999},
address = {Oldenburg},
month = {August},
note = {Nr. 6/99  ISSN 09462910},
postscript = {wittich99a.ps.gz} } 
[proceedings] bibtexTransformationBased Reactive Systems Development.
@PROCEEDINGS{LNCS1231, title = {{TransformationBased Reactive Systems Development}},
year = {1997},
editor = {M.~Bertran and T.~Rus},
volume = {1231},
series = {Lecture Notes in Computer Science},
address = {Mallorca, Spain},
publisher = {SpringerVerlag},
month = MAY } 
[proceedings] bibtexFME'97: Industrial Applications and Strengthened Foundations of Formal Methods.
@PROCEEDINGS{LNCS1313, title = {{FME'97: Industrial Applications and Strengthened Foundations of Formal Methods}},
year = {1997},
editor = {J.~Fitzgerald and C.B.~Jones and P.~Lucas},
volume = {1231},
series = {Lecture Notes in Computer Science},
address = {Graz, Austria},
publisher = {SpringerVerlag},
month = SEP } 
[proceedings] bibtexMathematics of Program Construction.
@PROCEEDINGS{LNCS1422, title = {{Mathematics of Program Construction}},
year = {1998},
editor = {J.~Jeuring},
volume = {1422},
series = {Lecture Notes in Computer Science},
month = JUN, optnumber = {1422},
optpublisher = {SpringerVerlag} } 
[proceedings] bibtexFormal Techniques in RealTime and FaultTolerant Systems.
@PROCEEDINGS{LNCS1135, title = {{Formal Techniques in RealTime and FaultTolerant Systems}},
year = {1996},
editor = {B.~Jonsson and J.~Parrow},
volume = {1135},
series = {Lecture Notes in Computer Science},
address = {Uppsala, Sweden},
publisher = {SpringerVerlag},
month = SEP } 
[proceedings] bibtexCompositionality: The Significant Difference.
@PROCEEDINGS{LNCS1536, title = {{Compositionality: The Significant Difference}},
year = {1998},
editor = {H.~Langmaack and A.~Pnueli and W.P.~de~Roever},
volume = {1536},
series = {Lecture Notes in Computer Science},
publisher = {SpringerVerlag} } 
[proceedings] bibtexFormal Techniques in RealTime and FaultTolerant Systems.
@PROCEEDINGS{LNCS1486, title = {{Formal Techniques in RealTime and FaultTolerant Systems}},
year = {1998},
editor = {A.P.~Ravn and H.~Rischel},
volume = {1486},
series = {Lecture Notes in Computer Science},
address = {Lyngby, Denmark},
publisher = {SpringerVerlag},
month = SEP } 
[proceedings] bibtexTenth International Symposium on System Synthesis.
@PROCEEDINGS{ISSS97, title = {{Tenth International Symposium on System Synthesis}},
year = {1997},
publisher = {IEEE CS Press},
month = SEP, key = {ISSS} }