Using a .NET Checkability Profile to Limit Interactions between Embedded Controllers

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.