车载分布式系统与应用软件的模型检测方法

OSEK/VDX, a development standard of vehicle-mounted system, has been widely adopted by many automotive manufacturers, such as Benz, BMW, etc. However, how to ensure the reliability of developed OSEK/VDX vehicle-mounted system is becoming a challenge in the industry of automobile software. Currently, model checking, as an exhaustive checking technique, is considered by automotive manufacturers in the verification process. Based on the model checking technique, although there exist several checking methods that can be employed to verify OSEK/VDX vehicle-mounted system, these existing methods just focus on the verification of OSEK/VDX OS. How to verify developed OSEK/VDX applications and distrusted application system is still at preliminary stage. Therefore, as to promote the development of automobile software, in our research we will propose an automatic checking approach to verify OSEK/VDX applications and distrusted application system based on the model checking technique.

OSEK/VDX作为一个车载系统的开发标准，已被汽车厂商广泛地采用，如奔驰、宝马等。然而，如何确保基于OSEK/VDX标准开发的车载软件系统可靠地运行，现已成为制约汽车软件工业发展的首要问题。模型检测作为一种保证软件可靠性的彻底验证技术，当前已被汽车厂商所关注。基于模型检测技术，国内外已提出一些检测方法以提高OSEK/VDX车载软件系统的可靠性。但现有方法大都聚焦于检测开发的OSEK/VDX操作系统，对于基于OSEK/VDX标准开发的应用软件与分布式应用软件系统的模型检测尚处于初级阶段。为此，本研究拟基于模型检测技术提出一个有效的自动化检测方法，以对汽车软件工业的发展做出贡献。

OSEK/VDX是应用于车载嵌入式系统的一个体系架构的标准，其既包含了实时性系统的特征也包含了分布式的特征。此标准现已经被汽车厂商广泛用于去实现一个单应用软件或分布式应用车载软件系统。然而，随着开发规模的剧增，开发者正面临一个挑战：如何完备地确保一个OSEK/VDX应用软件系统的可靠性。针对此问题，基于模型检查技术本项目提出了一个检查方法，该方法包含三个方面的优势：第一，相比较现有的检查方法，本项目提出的方法更加行之有效；第二，为提高本方法的检查能力，提出了两种优化策略；第三，基于提出的方法实现了一套自动化的验证工具，该工具可自动地完成目标系统的验证。