Edinburgh Research Explorer

A Novel WCET semantics of Synchronous Programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Access status

Open

Documents

http://link.springer.com/chapter/10.1007/978-3-319-44878-7_12
Original languageEnglish
Title of host publication Formal Modeling and Analysis of Timed Systems
Subtitle of host publication14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2016)
PublisherSpringer International Publishing
Pages195-210
Number of pages16
ISBN (Electronic)978-3-319-44878-7
ISBN (Print)978-3-319-44877-0
DOIs
StatePublished - 17 Aug 2016

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer International Publishing
Volume9884
ISSN (Print)0302-9743

Abstract

Semantics for synchronous programming languages are well known. They capture the execution behaviour of reactive systems using precise formal operational or denotational models for verification and unambiguous semantics-preserving compilation. As synchronous programs are highly time critical, there is an imminent need for the development of an execution time aware semantics that can be used as the formal basis of WCET tools. To this end we propose such a compositional semantics for synchronous programs. Our approach, which is algebraic and based on formal power series in min-max-plus algebra, combines in one setting both the linear system theory for timing and constructive Gödel Dummet logic for functional specification of synchronisation behaviour. The developed semantics is illustrated using a running example in the SCCharts language.

Download statistics

No data available

ID: 26473687