Modelling an Automotive Software-Intensive System with Adaptive Features Using ASMETA

被引：10

作者：

Arcaini, Paolo ^{[1
]}

Bonfanti, Silvia ^{[2
]}

Gargantini, Angelo ^{[2
]}

Riccobene, Elvinia ^{[3
]}

Scandurra, Patrizia ^{[2
]}

机构：

[1] Natl Inst Informat, Tokyo, Japan

[2] Univ Bergamo, Dept Econ & Technol Management, Informat Technol & Prod, Bergamo, Italy

[3] Univ Milan, Dipartimento Informat, Milan, Italy

来源：

RIGOROUS STATE-BASED METHODS, ABZ 2020 | 2020年 / 12071卷

关键词：

SIMULATION; LANGUAGE;

D O I：

10.1007/978-3-030-48077-6_25

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In the context of automotive domain, modern control systems are software-intensive and have adaptive features to provide safety and comfort. These software-based features demand software engineering approaches and formal methods that are able to guarantee correct operation, since malfunctions may cause harm/damage. Adaptive Exterior Light and the Speed Control Systems are examples of software-intensive systems that equip modern cars. We have used the Abstract State Machines to model the behaviour of both control systems. Each model has been developed through model refinement, following the incremental way in which functional requirements are given. We used the ASMETA tool-set to support the simulation of the abstract models, their validation against the informal requirements, and the verification of behavioural properties. In this paper, we discuss our modelling, validation and verification strategies, and the results (in terms of features addressed and not) of our activities. In particular, we provide insights on how we addressed the adaptive features (the adaptive high beam headlights and the adaptive cruise control) by explicitly modelling their software control loops according to the MAPE-K (Monitor-Analyse-Plan-Execute over a shared Knowledge) reference control model for self-adaptive systems.

引用

页码：302 / 317

页数：16

共 16 条

[1]

Arcaini P., 2012, RUNTIME VERIFICATION, V7186, DOI [10.1007/978-3-642-29860-8_17, DOI 10.1007/978-3-642-29860-8_17]

[2] Formal Design and Verification of Self-Adaptive Systems with Decentralized Control [J].

Arcaini, Paolo ;

Riccobene, Elvinia ;

Scandurra, Patrizia .

ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2017, 11 (04)

[3] A model-driven process for engineering a toolset for a formal method [J].

Arcaini, Paolo ;

Gargantini, Angelo ;

Riccobene, Elvinia ;

Scandurra, Patrizia .

SOFTWARE-PRACTICE & EXPERIENCE, 2011, 41 (02) :155-166

[4]

Arcaini P, 2010, LECT NOTES COMPUT SC, V5977, P61, DOI 10.1007/978-3-642-11811-1_6

[5]

Arcaini Paolo., 2010, NASA Formal Methods Symposium, P4

[6]

Blass A., 2003, ACM Transactions on Computational Logic, V4, P578, DOI 10.1145/937555.937561

[7] Design and validation of a C plus plus code generator from Abstract State Machines specifications [J].

Bonfanti, Silvia ;

Gargantini, Angelo ;

Mashkoor, Atif .

JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS, 2020, 32 (02)

[8]

Bonfanti S, 2018, LECT NOTES COMPUT SC, V10817, P369, DOI 10.1007/978-3-319-91271-4_25

[9]

Borger Egon, 2018, Modeling Companion for Software Practitioners, DOI [10.1007/978-3-662-56641-1, DOI 10.1007/978-3-662-56641-1]

[10]

Carioni A, 2008, LECT NOTES COMPUT SC, V5238, P71

← 1 2 →