ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 11:30 - 12:00 at JUPITER - Software Verification I Chair(s): Wil van der Aalst

The Clock Constraint Specification Language (CCSL) is a formalism for specifying logical-time constraints on events for the design of real-time embedded systems. A central verification problem of CCSL is to check whether events are schedulable under logical constraints. Although many efforts have been made addressing this problem, the problem is still open. In this paper, we show that the bounded scheduling problem is NP-complete and then propose an efficient SMT-based decision procedure which is sound and complete. Based on this decision procedure, we present a sound algorithm for the general scheduling problem. We implement our algorithm in a prototype tool and illustrate its utility in schedulability analysis in designing real-world systems and automatic proving of algebraic properties of CCSL constraints. Experimental results demonstrate its effectiveness and efficiency.

Tue 9 Apr

fase-2019-papers
10:30 - 12:30: FASE 2019 - Software Verification I at JUPITER
Chair(s): Wil van der AalstRWTH Aachen
fase-2019-papers10:30 - 11:00
Talk
Tobias RungeTU Braunschweig, Ina SchaeferTechnische Universität Braunschweig, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas ThümTU Braunschweig, Germany, Derrick KourieStellenbosch University, Bruce W Watson
Link to publication
fase-2019-papers11:00 - 11:30
Talk
Joonyoung Park, Alexander JordanOracle Labs, Australia, Sukyoung RyuKAIST, South Korea
Link to publication
fase-2019-papers11:30 - 12:00
Talk
Min ZhangEast China Normal University, Fu Song, Frederic MalletUniversité Côte d'Azur, France, Xiaohong Chen
Link to publication
fase-2019-papers12:00 - 12:30
Talk
Rolf HennickerLudwig Maximilians University Munich, Germany, Alexandre Madeira, Alexander Knapp
Link to publication