A Novel WCET semantics of Synchronous Programs

Michael Mendler, Partha S Roop, Bruno Bodin

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

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.
Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems
Subtitle of host publication14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2016)
Place of PublicationQuebec City, Canada
PublisherSpringer International Publishing
Pages195-210
Number of pages16
ISBN (Electronic)978-3-319-44878-7
ISBN (Print)978-3-319-44877-0
DOIs
Publication statusPublished - 17 Aug 2016
Event14th International Conference on Formal Modeling and Analysis of Timed Systems - Quebec City, Canada
Duration: 24 Aug 201626 Aug 2016

Publication series

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

Conference

Conference14th International Conference on Formal Modeling and Analysis of Timed Systems
Abbreviated titleFORMATS 2016
CountryCanada
CityQuebec City
Period24/08/1626/08/16

Fingerprint

Dive into the research topics of 'A Novel WCET semantics of Synchronous Programs'. Together they form a unique fingerprint.

Cite this