research-article

Schedulability analysis support for automotive systems: from requirement to implementation

Authors:

Eun-Young Kang,

Pierre-Yves SchobbensAuthors Info & Claims

SAC '14: Proceedings of the 29th Annual ACM Symposium on Applied Computing

Pages 1080 - 1085

https://doi.org/10.1145/2554850.2554929

Published: 24 March 2014 Publication History

Abstract

Modeling and analysis of precise non-functional properties, such as energy and timing constraints, is key to the correct development of automotive systems. Automotive applications development cost, in particular, is impacted by incorrect design made at the early development phases but only detected later, often after implementation. This late detection of design errors leads to additional cost. In this paper, we propose a model driven approach to perform non-functional properties verification and to enable scheduling analysis of automotive systems at the very early design level. The different phases of a design range from the requirements to a model allocated on a specific execution platform: East-adl and Marte are used together to specify the structure and energy/timing constraints of the software, as well as the hardware parts of the system. To prove the correctness of specification and perform the scheduling analysis, the semantics of the constraints is given as mapping to a formal interchange format Xfg (eXtended Function-block Graphs) language. The Xfg models are then automatically translated into priced timed automata for model checking. This later transformation is supported by a tool chain called A-BeTA. We demonstrate the applicability of our approach on the Brake-By-Wire case study.

References

[1]

R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid Automata. In Hybrid Systems, LNCS(736), pp 209--229, 1993.

Digital Library

[2]

R. Alur and D. L. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2): 183--235, 1994.

Digital Library

[3]

Automotive open system architecture. www.autosar.org.

[4]

G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, J. Romijn, and F. Vaandrager. Minimum-cost reachability for priced timed automata, In Hybrid Systems, LNCS(2034), pp 147--161, 2001.

Digital Library

[5]

P. Cuenot, P. Frey, R. Johansson, H. Lönn, M. Reiser, D. Servat, R. Koligari, and D. Chen. Developing automotive products using EAST-ADL2 and AUTOSAR compliant architecture description language. Ingeniurs de l'Automobile 793, pp 58--64, 2008.

[6]

EAST-ADL Specification v2.1.9. MAENAD Project 2011.

[7]

EAST-ADL White Paper M2. http://www.maenad.eu

[8]

H. Espinoza, H. Dubois, S. Gérard, J. Medina, D. Petriu, and M. Woodside. Annotating UML models with non-functional properties for quantitative analysis. In MoDELS, pp 79--90, LNCS(3844), 2006.

Digital Library

[9]

E. Y. Kang, E. Enois, R. Marinescu, C. Seceleanu, P. Y. Schobbens, and P. Pettersson. A methodology for formal analysis and verification of EAST-ADL models. Reliability Engineering and System Safety Journal, pp 127--138, 2013.

[10]

E. Y. Kang, G. Perrouin, and P. Y. Schobbens. Towards formal energy and time aware behaviors in EAST-ADL: An MDE approach. In QSIC, pp 124--127, IEEE, 2012.

Digital Library

[11]

E. Y. Kang, G. Perrouin, and P. Y. Schobbens. EAST-ADL behavioral modeling and its translation into the analyzable formal model. TR, PReCISE Center, Belgium, 2013.

[12]

E. Y. Kang, G. Perrouin, and P. Y. Schobbens. Model-based verification of energy-aware real-time automotive systems. In ICECCS, pp 135--144, IEEE, 2013.

Digital Library

[13]

E. Y. Kang and P. Y. Schobbens. Advanced XFG language: Extending XFG with energy-aware timed requirement properties. TR, PReCISE Centre, Belgium, 2013.

[14]

E. Y. Kang and P. Y. Schobbens. Extending EAST-ADL towards formal modeling and analysis of energy-aware real-time systems. In ICCA, pp 1890--1895, IEEE, 2013.

[15]

E. Y. Kang, P. Y. Schobbens, and P. Pettersson. Verifying functional behaviors of automotive products in EAST-ADL2 using UPPAAL-PORT. In SAFECOMP, pp 243--256, LNCS(6894), 2011.

Digital Library

[16]

MAENAD FP7 Project. http://www.maenad.eu/

[17]

F. Mallet, C. Andre, and R. Simone. CCSL: Specifying clock constraints with UML/MARTE. In ISSE, pp 309--314, 2008.

[18]

F. Mallet, M.-A. Peraldi-Frati, and C. Andre. MARTE CCSL to execute EAST-ADL timing requirements. In ISORC, pp 249--253, IEEE, 2009.

Digital Library

[19]

MARTE: Modeling and analysis of real-time embedded systems v 1.1., OMG, 2011.

[20]

A. Goknil, J. Suryadevara, M. A. Peraldi-Frati and F. Mallet. Analysis support for TADL2 timing constraints on EAST-ADL models, In ECSA, pp 89--105, LNCS(7957), 2013.

Digital Library

[21]

M. A. Peraldi-Frati, A. Goknil, J. DeAntoni, and J. Nordlander. A timing model for specifying multi clock automotive systems: TADL2. In ICECCS, pp 230--239, 2012.

Digital Library

[22]

Timing Augmented Description Language V2, 2010. http://www.timmo-2-use.org/timmo/publications.htm

[23]

TIMing MOdel, http://www.timmo-2-use.org

Cited By

Kang E(2023)ASSA-CPS: Automated Formal Safety and Security Assessments in Cyber-Physical Systems2023 7th International Conference on System Reliability and Safety (ICSRS)10.1109/ICSRS59833.2023.10381141(518-522)Online publication date: 22-Nov-2023
https://doi.org/10.1109/ICSRS59833.2023.10381141
Kang EBrix MSzenczi DKováts ÁFormosa RMelsen CNørgård M(2022)Model-Driven Software Development Approach: Ensuring Safety of an IoT-Based Plant Health Monitoring System2022 6th International Conference on System Reliability and Safety (ICSRS)10.1109/ICSRS56243.2022.10067493(251-258)Online publication date: 23-Nov-2022
https://doi.org/10.1109/ICSRS56243.2022.10067493
Zhang HFeng LLi Z(2020)Control of Black-Box Embedded Systems by Integrating Automaton Learning and Supervisory Control Theory of Discrete-Event SystemsIEEE Transactions on Automation Science and Engineering10.1109/TASE.2019.292956317:1(361-374)Online publication date: Jan-2020
https://doi.org/10.1109/TASE.2019.2929563
Show More Cited By

Index Terms

Schedulability analysis support for automotive systems: from requirement to implementation

Recommendations

Applicability of real-time schedulability analysis on a software radio protocol
HILT '12: Proceedings of the 2012 ACM conference on High integrity language technology

In this paper, we present our experience on integrating timing constraint verification and analysis, by using the real-time scheduling theory, in an industrial context. The verification process has been integrated into a design flow at THALES ...
Applicability of real-time schedulability analysis on a software radio protocol
HILT '12

In this paper, we present our experience on integrating timing constraint verification and analysis, by using the real-time scheduling theory, in an industrial context. The verification process has been integrated into a design flow at THALES ...
Verifying MARTE/CCSL Mode Behaviors Using UPPAAL
SEFM 2013: Proceedings of the 11th International Conference on Software Engineering and Formal Methods - Volume 8137

In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the systems overall timing behavior. To support the design and analysis ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '14: Proceedings of the 29th Annual ACM Symposium on Applied Computing

March 2014

1890 pages

ISBN:9781450324694

DOI:10.1145/2554850

Conference Chairs:
Yookun Cho
Seoul National University, Korea
,
Sung Y. Shin
South Dakota State University
,
Program Chairs:
Sangwook Kim
Kyungpook National University, Korea
,
Chih-Cheng Hung
Southern Polytechnic State University
,
Jiman Hong
Soongsil University, South Korea

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 March 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2014

Sponsor:

SIGAPP

SAC 2014: Symposium on Applied Computing

March 24 - 28, 2014

Gyeongju, Republic of Korea

Acceptance Rates

SAC '14 Paper Acceptance Rate 218 of 939 submissions, 23%;

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
137
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kang E(2023)ASSA-CPS: Automated Formal Safety and Security Assessments in Cyber-Physical Systems2023 7th International Conference on System Reliability and Safety (ICSRS)10.1109/ICSRS59833.2023.10381141(518-522)Online publication date: 22-Nov-2023
https://doi.org/10.1109/ICSRS59833.2023.10381141
Kang EBrix MSzenczi DKováts ÁFormosa RMelsen CNørgård M(2022)Model-Driven Software Development Approach: Ensuring Safety of an IoT-Based Plant Health Monitoring System2022 6th International Conference on System Reliability and Safety (ICSRS)10.1109/ICSRS56243.2022.10067493(251-258)Online publication date: 23-Nov-2022
https://doi.org/10.1109/ICSRS56243.2022.10067493
Zhang HFeng LLi Z(2020)Control of Black-Box Embedded Systems by Integrating Automaton Learning and Supervisory Control Theory of Discrete-Event SystemsIEEE Transactions on Automation Science and Engineering10.1109/TASE.2019.292956317:1(361-374)Online publication date: Jan-2020
https://doi.org/10.1109/TASE.2019.2929563
Kang ESchobbens P(2020)InFoCPS: Integrating Formal Analysis of Cyber-Physical Systems with Energy Prognostics2020 9th Mediterranean Conference on Embedded Computing (MECO)10.1109/MECO49872.2020.9134341(1-5)Online publication date: Jun-2020
https://doi.org/10.1109/MECO49872.2020.9134341
Hu MWei TZhang MMallet FChen M(2019)Sample-Guided Automated Synthesis for CCSL SpecificationsProceedings of the 56th Annual Design Automation Conference 201910.1145/3316781.3317904(1-6)Online publication date: 2-Jun-2019
https://dl.acm.org/doi/10.1145/3316781.3317904
Zhang YMallet FZhu HChen Y(2019)A Logical Approach for the Schedulability Analysis of CCSL2019 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2019.00-23(25-32)Online publication date: Jul-2019
https://doi.org/10.1109/TASE.2019.00-23
Huang LLiang TKang E(2019)Formal Verification of Dynamic and Stochastic Behaviors for Automotive Systems2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS.2019.00009(11-20)Online publication date: Nov-2019
https://doi.org/10.1109/ICECCS.2019.00009
Zhang MSong FMallet FChen X(2019)SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification LanguageFundamental Approaches to Software Engineering10.1007/978-3-030-16722-6_4(61-78)Online publication date: 4-Apr-2019
https://doi.org/10.1007/978-3-030-16722-6_4
Kang EHuang LMu DHaddad HWainwright RChbeir R(2018)Formal verification of energy and timed requirements for a cooperative automotive systemProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167291(1492-1499)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167291
Zhang HFeng LWu NLi Z(2018)Integration of Learning-Based Testing and Supervisory Control for Requirements Conformance of Black-Box Reactive SystemsIEEE Transactions on Automation Science and Engineering10.1109/TASE.2017.269399515:1(2-15)Online publication date: Jan-2018
https://doi.org/10.1109/TASE.2017.2693995
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents