← Back to program

Embedded- and Real-Time Systems

Session introduction · Tuesday, 15:30-17:00 · Chair: Levente Bajczi

This session is about embedded and real-time systems, often in settings where a fault is dangerous or expensive. Making such systems trustworthy is the thread that runs through the talks.

One widely used embedded controller is the programmable logic controller (PLC), an industrial computer that runs its program in a repeating scan cycle [1]. For such control code, engineers rely mostly on dynamic testing, which runs the program on chosen inputs, while formal methods can add proofs that cover every input. Mutation testing measures how good a test suite is. It injects small faults, called mutants, and checks whether the tests catch them, so a mutant that survives every test marks a gap in the suite [2]. Some mutants are equivalent, meaning they change the code but not its behaviour, so no test can ever catch them, and finding these automatically is hard [2]. A model checker can help on both sides, by generating tests for surviving mutants and by identifying equivalent ones [3].

Timing is a first-class concern in this session. A real-time system must be correct and on time, because a late answer can count as a wrong one, and a hard deadline must never be missed [4]. Timed Automata are the standard model for such systems: state machines extended with clocks, which a tool can then check automatically [5]. A separate analysis, worst-case execution time (WCET), computes a safe upper bound on how long a piece of code can run [6]. These concerns are usually handled apart, because a program verifier tends to ignore time while a timing model tends to ignore the program's memory and synchronisation, so merging them into one analysis is hard [6]. Timing also matters in hardware. In a digital circuit, a signal takes time to pass through each gate, and timing analysis predicts when the outputs settle [7]. Rather than simulate one input pattern at a time, symbolic execution explores many input orderings together using symbolic values [8, 9]. This is powerful, but it produces a combinatorial explosion of cases that such methods must prune.

A final question is what a component may assume about its surroundings. If we verify a component against an environment that is allowed to do anything, the checker often reports failures that could never happen in practice. The remedy is to state environment assumptions explicitly, in an assume-guarantee style: we assume some behaviour of the environment, and in return guarantee some behaviour of the component [10]. Such assumptions can be written in linear temporal logic (LTL), a logic for describing how a system should behave over time [11]. Writing good assumptions by hand is difficult, so recent work synthesizes them automatically [10].

Keywords to look up: embedded system · programmable logic controller (PLC) · safety-critical · dynamic testing · mutation testing · equivalent mutant · test generation · model checking · real-time system · deadline · Timed Automata · clock · worst-case execution time (WCET) · environment assumption · assume-guarantee · linear temporal logic (LTL) · assumption synthesis · digital circuit · gate delay · symbolic execution · combinatorial explosion.

Sources

  1. B. Fernández Adiego, D. Darvas, E. Blanco Viñuela, J.-C. Tournier, S. Bliudze, J. O. Blech, V. M. González Suárez. "Applying Model Checking to Industrial-Sized PLC Programs." IEEE Trans. Industrial Informatics, 2015. doi.org/10.1109/TII.2015.2489184
  2. Y. Jia, M. Harman. "An Analysis and Survey of the Development of Mutation Testing." IEEE Trans. Software Engineering, 2011. doi.org/10.1109/TSE.2010.62
  3. G. Fraser, F. Wotawa, P. E. Ammann. "Testing with Model Checkers: A Survey." Software Testing, Verification and Reliability, 2009. doi.org/10.1002/stvr.402
  4. G. C. Buttazzo. Hard Real-Time Computing Systems. Springer, 3rd ed., 2011. doi.org/10.1007/978-1-4614-0676-1
  5. R. Alur, D. L. Dill. "A Theory of Timed Automata." Theoretical Computer Science, 1994. doi.org/10.1016/0304-3975(94)90010-8
  6. R. Wilhelm et al. "The Worst-Case Execution-Time Problem - Overview of Methods and Survey of Tools." ACM Trans. Embedded Computing Systems, 2008. doi.org/10.1145/1347375.1347389
  7. J. Bhasker, R. Chadha. Static Timing Analysis for Nanometer Designs. Springer, 2009. doi.org/10.1007/978-0-387-93820-2
  8. J. C. King. "Symbolic Execution and Program Testing." Communications of the ACM, 1976. doi.org/10.1145/360248.360252
  9. R. Baldoni, E. Coppa, D. C. D'Elia, C. Demetrescu, I. Finocchi. "A Survey of Symbolic Execution Techniques." ACM Computing Surveys, 2018. doi.org/10.1145/3182657
  10. K. Chatterjee, T. A. Henzinger, B. Jobstmann. "Environment Assumptions for Synthesis." CONCUR, 2008. doi.org/10.1007/978-3-540-85361-9_14
  11. A. Pnueli. "The Temporal Logic of Programs." FOCS, 1977. doi.org/10.1109/SFCS.1977.32