You are here

Home › Research › Publications ›

Runtime Verification of AUTOSAR Timing Extensions

TitleRuntime Verification of AUTOSAR Timing Extensions
Publication TypeConference Paper
Year of Publication2022
AuthorsFriese, MJonas, Kallwies, H, Leucker, M, Sachenbacher, M, Streichhahn, H, Thoma, D
Conference Name30th International Conference on Real-Time Networks and Systems (RTNS)
Date Published06/2022
PublisherACM
Conference LocationParis, France
KeywordsAutomotive, AUTOSAR, Runtime verification
Abstract

Meeting timing requirements is essential for the correct behavior of embedded systems in today's vehicles.
In the automotive domain, the AUTOSAR Timing Extensions are a widely used and accepted standard for specifying timing requirements.
Previous work focused on defining such timing constraints in a mathematically precise way, using timing-augmented description languages such as TADL2, in order to perform offline system analysis such as automated model checking and verification.
However, not all types of timing specification violations can be detected at system development time, and sporadic rare events require a capability for long-term observation of system behavior.
Runtime verification is a formal method that considers actual runs of a system, as opposed to static analysis, and checks properties on streams of events using monitors constructed from specifications.

In this paper, we investigate how runtime verification can be used to monitor AUTOSAR timing constraints on system traces.
First, we analyze the complexity of monitoring different types of AUTOSAR and related TADL2 timing constraints, finding that the constraints belong to different classes defined by the resources required for monitoring.
Second, we present a library of timing specifications that implements the AUTOSAR and TADL2 constraints in the temporal stream-based specification language TeSSLa. From these TeSSLa specifications, monitors can then be automatically generated and either compiled to a Scala program executed on the JVM, or alternatively run on specialized hardware such as FPGAs.
Finally, experimental results are presented where timing specifications are monitored on synthetically generated traces and real-world traces obtained from an industrial automotive application.
URLhttps://dl.acm.org/doi/10.1145/3534879.3534898
DOI10.1145/3534879.3534898
Bibtex: 
@inproceedings {1410,
	title = {Runtime Verification of AUTOSAR Timing Extensions},
	booktitle = {30th International Conference on Real-Time Networks and Systems (RTNS)},
	year = {2022},
	month = {06/2022},
	publisher = {ACM},
	organization = {ACM},
	address = {Paris, France},
	abstract = {<p>Meeting timing requirements is essential for the correct behavior of embedded systems in today{\textquoteright}s vehicles.<br>
	In the automotive domain, the AUTOSAR Timing Extensions are a widely used and accepted standard for specifying timing requirements.<br>
	Previous work focused on defining such timing constraints in a mathematically precise way, using timing-augmented description languages such as TADL2, in order to perform offline system analysis such as automated model checking and verification.<br>
	However, not all types of timing specification violations can be detected at system development time, and sporadic rare events require a capability for long-term observation of system behavior.<br>
	Runtime verification is a formal method that considers actual runs of a system, as opposed to static analysis, and checks properties on streams of events using monitors constructed from specifications.</p>
<p>In this paper, we investigate how runtime verification can be used to monitor AUTOSAR timing constraints on system traces.<br>
	First, we analyze the complexity of monitoring different types of AUTOSAR and related TADL2 timing constraints, finding that the constraints belong to different classes defined by the resources required for monitoring.<br>
	Second, we present a library of timing specifications that implements the AUTOSAR and TADL2 constraints in the temporal stream-based specification language TeSSLa. From these TeSSLa specifications, monitors can then be automatically generated and either compiled to a Scala program executed on the JVM, or alternatively run on specialized hardware such as FPGAs.<br>
	Finally, experimental results are presented where timing specifications are monitored on synthetically generated traces and real-world traces obtained from an industrial automotive application.</p>
},
	keywords = {Automotive, AUTOSAR, Runtime verification},
	doi = {10.1145/3534879.3534898},
	url = {https://dl.acm.org/doi/10.1145/3534879.3534898},
	author = {Max Jonas Friese and Hannes Kallwies and Martin Leucker and Martin Sachenbacher and Hendrik Streichhahn and Daniel Thoma}
}