This paper shows an approach for software synthesis in embedded hard real-time systems starting from Live Sequence Charts (LSC) scenarios as specification language. As the name suggests, LSCs specify liveness, that is, things that must happen. Therefore allowing the distinction between possible and necessary behavior as well as the specification of possible anti-scenarios. Embedded software has become much harder to design due to the diversity of requirements and high complexity. In such systems, correctness and timeliness verification is an issue to be concerned. The software synthesis method takes a specification (in this case composed by LSC scenarios) and automatically generates a program source code where: (ⅰ) functionalities and constraints are satisfied; and (ⅱ) operational support for task's execution is provided. This paper adopts a time Petri net (TPN) formalism for system modeling in order to find feasible pre-runtime schedules, and for synthesizing predictable and timely scheduled code. Embedded software synthesis has been receiving much attention. However, few works deal with software synthesis for hard real-time systems considering arbitrary precedence and exclusion relations.
展开▼
