Verifiable COTS-based cyber-physical systems

Cyber-physical systems (CPS) use networked control software to interact with and manipulate the physical world. Examples of cyber-physical systems include smart buildings, power distribution networks, and fleets of autonomous agriculture vehicles. These types of systems are increasingly of interest due to the significant potential benefit of automating and optimizing tasks in the real-world and at large scales. However, before wide-scale deployment becomes a reality, two challenges must be addressed: safety and cost. The contained research directly addresses these two challenges, in the context of cyber-physical systems. The second challenge of cyber-physical systems is their cost. Since cyber-physical systems interact with the physical world, these systems are often inherently real-time systems. In real-time systems, the correctness of a computation is not only a function of its result, but also depends on the timing at which the result is produced. For example, an inherently unstable airplane, like the F-16, needs a control system that can guarantee adjustments are always made dozens of times a second in order to guarantee aircraft stability. Most commercial off-the-shelf (COTS) computing systems, however, do not provide such real-time guarantees. Relying on custom-made components in order to guarantee timeliness properties, however, leads to systems with an exorbitant cost. For affordability, we must make use of low-cost COTS components. In the presented research, we address the primary problem with COTS components used in real-time systems: unpredictable interference, and therefore unpredictable timing, when accessing a shared memory resource. Methods are provided to mitigate both memory interference from external peripherals, as well as memory interference from other cores in a multi-core processor. Since cyber-physical systems interact with the physical world, the effects of bugs in the design or implementation are not necessarily quarantined in the cyber (software) part of the system. Software written with traditional development practices will almost certainly contain bugs or unintended interactions among components. In CPS, these bugs can result in uncontrolled and possibly disastrous physical-world interactions. The safety problem for CPS is addressed on two fronts. First, a technique based on selective command filtering is provided to give safety to the high-level CPS computation. This technique can guarantee distributed safety properties in the physical world, if assumptions are given about the low-level controllers. Second, a method for guaranteeing assumptions about the low-level controllers is presented. This method, based on the Simplex Architecture, allows safety invariants to be maintained in individual agents of the distributed CPS, despite the presence of bugs in their control software. Combined, the two approaches provide safety for entire CPS, without requiring complete formal verification of the system.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2013

Author dc:creator

• Bak, Stanley

Contributors dc:contributor

• Caccamo, Marco
• Mitra, Sayan
• Sha, Lui R.
• Hill, James

• real-time
• cyber-physical system
• verification
• simplex
• system-level simplex
• architecture
• safety
• off-road vehicle
• hybrid system
• hybrid automaton
• nonlinear
• reachability
• Commercial off-the-shelf (COTS)
• real-time bridge
• memory interference

Statement dc:rights

• Copyright 2013 Stanley Bak

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/44374

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/44374