Many are the works proposed on timing and schedulability analysis for guaranteeing the predictability of single- and multi-core systems. The increasing complexity of embedded and real-time systems requires a continuous development in design and verification.

Formal methods are mathematics-based techniques for the specification, development and verification of software and hardware systems. In a certification context, industrials are more and more encouraged to apply formal methods such as model checking, abstract interpretation, etc. to guarantee the fulfillment of system requirements.

Applied to real-time, formal methods can be used to model real-time task behaviors, model task interactions and encode real-time requirements/properties such as timing constraints. They bring formal verification to timing and schedulability analysis of embedded and real-time systems.

The Formal Techniques for Real-Time Systems (FORTRESS) workshop provides a venue for bringing together researchers and developers from academia and industry to promote cross-fertilization and discuss advances dealing with the application of formal methods to embedded and real-time systems. Of particular interest are ideas and contributions that present significant paradigm shifts, explore unique and unconventional approaches to important problems, or investigate fundamental departures from conventional wisdom in adopted solutions.