Model Checking is Possible to Verify Large-scale Vehicle Distributed Application Systems

被引：0
|
作者：
Zhang, Haitao [1 ]
Tuo, Ayang [1 ]
Li, Guoqiang [2 ]
机构：
[1] Lanzhou Univ, Sch Informat Sci & Engn, Lanzhou 730000, Gansu, Peoples R China
[2] Shanghai Jiao Tong Univ, Sch Software, Shanghai 200240, Peoples R China
来源：
2019 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE) | 2019年
基金：
美国国家科学基金会;
关键词：
D O I：
10.23919/date.2019.8714795
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
OSEK/VDX is a specification for vehicle-mounted systems. Currently, the specification has been widely adopted by many automotive companies to develop a distributed vehicle application system. However, the ever increasing complexity of the developed distributed application system has created a challenge for exhaustively ensuring its reliability. Model checking as an exhaustive technique has been applied to verify OSEK/VDX distributed application systems to discover subtle errors. Unfortunately, it faces a poor scalability for practical systems because the verification models derived from such systems are highly complex. This paper presents an efficient approach that addresses this problem by reducing the complexity of the verification model such that model checking can easily complete the verification.
引用
收藏
页码：594 / 597
页数：4
相关论文
共 50 条
  • [1] Model checking large-scale and parameterized resource allocation systems
    Emerson, EA
    Kahlon, V
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 251 - 265
  • [2] Efficient Large-Scale Model Checking
    Verstoep, Kees
    Bal, Henri E.
    Barnat, Jiri
    Brim, Lubos
    [J]. 2009 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL & DISTRIBUTED PROCESSING, VOLS 1-5, 2009, : 201 - +
  • [3] Distributed model predictive control of large-scale systems
    Venkat, Aswin N.
    Rawlings, James B.
    Wright, Stephen J.
    [J]. ASSESSMENT AND FUTURE DIRECTIONS OF NONLINEAR MODEL PREDICTIVE CONTROL, 2007, 358 : 591 - +
  • [4] Distributed model predictive control for large-scale systems
    Du, XN
    Xi, YG
    Li, SY
    [J]. PROCEEDINGS OF THE 2001 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2001, : 3142 - 3143
  • [5] An I/O Efficient Model Checking Algorithm for Large-Scale Systems
    Wu, Lijun
    Huang, Huijia
    Su, Kaile
    Cai, Shaowei
    Zhang, Xiaosong
    [J]. IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2015, 23 (05) : 905 - 915
  • [6] Large-scale directed model checking LTL
    Edelkamp, S
    Jabbar, S
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2006, 3925 : 1 - 18
  • [7] Experiences from Large-Scale Model Checking: Verifying a Vehicle Control System with NuSMV
    Fritzsch, Jonas
    Schmid, Tobias
    Wagner, Stefan
    [J]. 2021 14TH IEEE CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2021), 2021, : 372 - 382
  • [8] A macroeconomic model for resource allocation in large-scale distributed systems
    Bai, Xin
    Marinescu, Dan C.
    Boloni, Ladislau
    Siegel, Howard Jay
    Daley, Rose A.
    Wang, I-Jeng
    [J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2008, 68 (02) : 182 - 199
  • [9] Implicit model Checking: Formal verification technique for large-scale discrete systems
    Park, T
    [J]. PROCEEDINGS OF THE 2000 IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER-AIDED CONTROL SYSTEM DESIGN, 2000, : 135 - 140
  • [10] Markov Chains Competing for Transitions: Application to Large-Scale Distributed Systems
    Anceaume, Emmanuelle
    Castella, Francois
    Ludinard, Romaric
    Sericola, Bruno
    [J]. METHODOLOGY AND COMPUTING IN APPLIED PROBABILITY, 2013, 15 (02) : 305 - 332
12345