AbsInt Angewandte Informatik. Worst-Case Execution Time Analyzers.
The AutoFocus^3 homepage.
http://af3.fortiss.org.
J. Botaschanjan, M. Broy, A. Gruler, A. Harhurin, S. Knapp, L. Kof, W. Paul & M. Spichkova (2008):
On the Correctness of Upper Layers of Automotive Systems.
Formal Aspects of Computing (FACS) 20(6),
pp. 637–662,
doi:10.1007/s00165-008-0097-0.
J. Botaschanjan, A. Gruler, A. Harhurin, L. Kof, M. Spichkova & D. Trachtenherz (2006):
Towards Modularized Verification of Distributed Time-Triggered Systems.
In: FM 2006: Formal Methods,
pp. 163–178,
doi:10.1007/11813040_12.
J. Botaschanjan, L. Kof, C. Kühnel & M. Spichkova (2005):
Towards Verified Automotive Software.
In: 2nd International ICSE workshop on Software.
ACM,
doi:10.1145/1082983.1083199.
M. Broy & K. Stølen (2001):
Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement.
Springer.
J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs & Y. Xiong (2003):
Taming heterogeneity - the Ptolemy approach.
Proc. of the IEEE 91(1),
pp. 127–144,
doi:10.1109/JPROC.2002.805829.
M. Feilkas, F. Hölzl, C. Pfaller, S. Rittmann, K. Scheidemann, M. Spichkova & D. Trachtenherz (2009):
A Top-Down Methodology for the Development of Automotive Software.
Tech. Rep. TUM-I0902.
TU München.
A. Fleischmann (2008):
Model-based formalization of requirements of embedded automotive systens.
TU München.
D. Harel & P. S. Thiagarajan (2003):
Message Sequence Charts.
In: L. Lavagno, G. Martin & B. Selic: UML for Real: Design of Embedded Real-Time Systems.
Kluwer Academic Publishers,
pp. 77–105.
C. Hofmann, E. Horn, W. Keller, K. Renzel, M. Schmidt, W. Horn & B. Anger:
Approaches to Software Architecture.
F. Hölzl (2009):
The AutoFocus 3 C0 Code Generator.
Tech. Rep. TUM-I0918.
TU München.
M. Jackson (2001):
Problem Frames: Analysing and Structuring Software Development Problems.
Addison-Wesley.
C. Kühnel & M. Spichkova (2007):
Fault-Tolerant Communication for Distributed Embedded Systems.
In: Software Engineering and Fault Tolerance,
Series on Software Engineering and Knowledge Engineering.
D. Leinenbach (2008):
Compiler Verification in the Context of Pervasive System Verification.
Saarland University.
O. Müller & T. Nipkow (1995):
Combining Model Checking and Deduction for I/O-Automata.
In: Ed Brinksma, R. Cleaveland, K. G. Larsen, T. Margaria & B. Steffen: TACAS,
LNCS 1019.
Springer,
pp. 1–16,
doi:10.1.1.11.1585.
T. Nipkow, L. C. Paulson & M. Wenzel (2002):
Isabelle/HOL – A Proof Assistant for Higher-Order Logic.
LNCS 2283.
Springer,
doi:10.1007/3-540-45949-9.
D. L. Parnas & J. Madey (1995):
Functional Documents for Computer Systems.
Science of Computer Programming 25,
pp. 41–61,
doi:10.1016/0167-6423(95)96871-J.
E. Petrova (2007):
Verification of the C0 Compiler Implementation on the Source Code Level.
J. Philipps & B. Rumpe (1999):
Refinement of Pipe-and-Filter Architectures.
In: J. M. Wing, J. Woodcock & J. Davies: World Congress on Formal Methods (FM'99) LNCS 1708.
Springer,
pp. 96 – 115,
doi:10.1007/3-540-48119-2_8.
B. Schätz (2004):
Mastering the Complexity of Reactive Systems: the AutoFocus Approach.
In: Formal Methods for Embedded Distributed Systems: How to Master the Complexity.
Kluwer Academic Publishers,
pp. 215–258.
N. Schirmer (2006):
Verification of Sequential Imperative Programs in Isabelle/HOL.
TU München.
M. Spichkova (2007):
Specification and Seamless Verification of Embedded Real-Time Systems: FOCUS on Isabelle.
TU München.
M. Spichkova (2010):
From Semiformal Requirements To Formal Specifications via MSCs.
Technical Report TUM-I1019.
TU München.
D. Trachtenherz (2009):
Ausführungssemantik von AutoFocus-Modellen: Isabelle/HOL-Formalisierung und Äquivalenzbeweis.
Tech. Rep. TUM-I0903.
TU München.
D. Wild, A. Fleischmann, J. Hartmann, C. Pfaller, M. Rappl & S. Rittmann (2006):
An Architecture-Centric Approach towards the Construction of Dependable Automotive Software.
In: Proc. of the SAE 2006 World Congress,
doi:10.4271/2006-01-1222.