skip to main content
10.1145/1083190.1083199acmotherconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
Article

Towards verified automotive software

Published: 21 May 2005 Publication History

Abstract

Automotive software is one of the most challenging fields of software engineering: it must meet real time requirements, is safety critical and distributed over multiple processors. With the increasing complexity of automotive software, as for example in the case of drive-by-wire, automated driving and driver assitents, software correctness becomes more and more a crucial issue. In order that these innovations can become reality, it is necessary to be able to guarantee software correctness.The presented work aims at verification of automotive software. For this purpose it introduces a verification approach, including a framework of verified modules which assists the verification of the actual application. Feasibility of this approach was validated on a case study that also showed how verification can be integrated into the development process.

References

[1]
FlexRay Consortium. FlexRay Communication System - Protocol Specification - Version 2.0, 2004.
[2]
P. Caspi, A. Curic, A. Maignan, C. Sofronis, S. Tripakis, and P. Niebert. From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications. In LCTES '03: Proceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, pages 153--162. ACM Press, 2003.
[3]
European Commission (DG Enterprise and DG Information Society). eSafety forum: Summary report 2003, March 2003.
[4]
FlexRay Consortium. http://www.flexray.com.
[5]
FlexRay Consortium. FlexRay Communication System - Bus Guardian Specification - Version 2.0, 2004.
[6]
M. Hillebrand. Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, 2005.
[7]
F. Huber, B. Schätz, and G. Einert. Consistent Graphical Specification of Distributed Systems. In J. Fitzgerald, C. Jones, and P. Lucas, editors, Industrial Applications and Strengthened Foundations of Formal Methods (FME97), LNCS 1313, pages 122--141. Springer Verlag, 1997.
[8]
L4 microkernel. http://os.inf.tu-dresden. de/L4/.
[9]
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
[10]
OSEK/VDX. http://www.osek-vdx.org.
[11]
OSEK/VDX. Fault-Tolerant Communication - Specification 1.0, 2001.
[12]
OSEK/VDX. Time-Triggered Operating System - Specification 1.0, 2001.
[13]
A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of LNCS, page 151. Weizmann Institute of Science, Rehovot, Israel, 1998.
[14]
J. Rushby. An overview of formal verification for the time-triggered architecture. In W. Damm and E.-R. Olderog, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 2469 of Lecture Notes in Computer Science, pages 83--105, Oldenburg, Germany, Sept. 2002. Springer-Verlag.
[15]
B. Schätz, A. Pretschner, F. Huber, and J. Philipps. Model-based development of embedded systems. In J.-M. Bruel and Z. Bellahsene, editors, Advances in Object-Oriented Information Systems. Springer, 2002.
[16]
S. Tverdyshev. Documentation and modelling of the ipc mechanism in the 14 kernel. Master's thesis, 2003.
[17]
Verisoft Project. http://www.verisoft.de/.

Cited By

View all
  • (2011)Formal Verification of SLA TransformationsProceedings of the 2011 IEEE World Congress on Services10.1109/SERVICES.2011.16(540-547)Online publication date: 4-Jul-2011
  • (2008)A language for advanced protocol analysis in automotive networksProceedings of the 30th international conference on Software engineering10.1145/1368088.1368171(593-602)Online publication date: 15-May-2008
  • (2008)On the correctness of upper layers of automotive systemsFormal Aspects of Computing10.1007/s00165-008-0097-020:6(637-662)Online publication date: 25-Nov-2008
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences
SEAS '05: Proceedings of the second international workshop on Software engineering for automotive systems
May 2005
58 pages
ISBN:1595931287
DOI:10.1145/1083190
  • cover image ACM SIGSOFT Software Engineering Notes
    ACM SIGSOFT Software Engineering Notes  Volume 30, Issue 4
    July 2005
    1514 pages
    ISSN:0163-5948
    DOI:10.1145/1082983
    Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 May 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. automotive
  2. integration
  3. model based software engineering
  4. theorem proving
  5. time-triggered
  6. verification

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2011)Formal Verification of SLA TransformationsProceedings of the 2011 IEEE World Congress on Services10.1109/SERVICES.2011.16(540-547)Online publication date: 4-Jul-2011
  • (2008)A language for advanced protocol analysis in automotive networksProceedings of the 30th international conference on Software engineering10.1145/1368088.1368171(593-602)Online publication date: 15-May-2008
  • (2008)On the correctness of upper layers of automotive systemsFormal Aspects of Computing10.1007/s00165-008-0097-020:6(637-662)Online publication date: 25-Nov-2008
  • (2008)Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)Leveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-540-88479-8_1(1-13)Online publication date: 2008
  • (2007)Engineering Automotive SoftwareProceedings of the IEEE10.1109/JPROC.2006.88838695:2(356-373)Online publication date: Feb-2007
  • (2007)Verification of clock synchronization algorithms: experiments on a combination of deductive toolsFormal Aspects of Computing10.1007/s00165-007-0027-619:3(321-341)Online publication date: 25-Jul-2007
  • (2006)Challenges in automotive software engineeringProceedings of the 28th international conference on Software engineering10.1145/1134285.1134292(33-42)Online publication date: 28-May-2006
  • (2006)SALT—structured assertion language for temporal logicProceedings of the 8th international conference on Formal Methods and Software Engineering10.1007/11901433_41(757-775)Online publication date: 1-Nov-2006
  • (2006)Towards modularized verification of distributed time-triggered systemsProceedings of the 14th international conference on Formal Methods10.1007/11813040_12(163-178)Online publication date: 21-Aug-2006
  • (2005)Towards the Formal Verification of Lower System Layers in Automotive SystemsProceedings of the 2005 International Conference on Computer Design10.1109/ICCD.2005.110(317-326)Online publication date: 2-Oct-2005
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media