Using a .NET Checkability Profile to Limit Interactions between Embedded Controllers
SENSORCOMM '08 Proceedings of the 2008 Second International Conference on Sensor Technologies and Applications(2008)
摘要
Within a closed domain - such as a railway train, chemical production line, vehicle or home of the future - concurrent applications running in embedded controller units (ECUs) and on servers share many common sensors, actuators and feedback paths through the physical part of the domain, while having to abide by common, basic liveness and consistency rules to ensure proper operation of that domain. This paper suggests that all ECUs must export a summary of their behaviour using a restricted subset of .NET bytecode and that the programming constructs used by all participating controllers must abide within a common upper bound so that automated formal checking of domain as a whole is possible. The upper bound is defined as a checkability profile. We describe the ROM and RAM costs of implementing this approach in one of our prototypes: a CD/DVD player for the home of the future.
更多查看译文
关键词
embedded systems,microcontrollers,.NET bytecode,.NET checkability profile,chemical production line,concurrent applications,consistency rules,embedded controller units,railway train,.NET,Application Digest,CLR,Feature Interaction.,Incremental Model Checking,Pervasive Computing,
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络