Giotto is a programming language to describe the behavior of distributed real-time embedded systems. Giotto has a formally defined time-triggered semantics which supports embedded programming at a high level of abstraction. In fact, a Giotto program provides an architecture-independent and thus logical view of an embedded system.
In this talk we will focus on Giotto's semantics. The key objects are concurrent periodic tasks and modes. A Giotto program consists of a set of modes where each mode contains a set of tasks. A distributed embedded system described by a Giotto program can only be in a single mode at the same time. The decision to perform a mode switch is based on sampling changes in the environment.
Future objectives are formal verification of real-time properties of Giotto programs using a refinement relation to the modeling language Masaccio, as well as annoted versions of Giotto allowing for architecture-dependent refinements of Giotto.