TY - GEN
T1 - An executable semantics of clock constraint specification language and its applications
AU - Zhang, Min
AU - Mallet, Frédéric
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of ccsl in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: (1) to automatically find bounded or periodic schedules that satisfy all the given constraints; (2) to simulate the execution of schedules with customized simulation policies; and (3) to verify LTL properties of ccsl constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of ccsl are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.
AB - The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of ccsl in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: (1) to automatically find bounded or periodic schedules that satisfy all the given constraints; (2) to simulate the execution of schedules with customized simulation policies; and (3) to verify LTL properties of ccsl constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of ccsl are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.
UR - https://www.scopus.com/pages/publications/84958965275
U2 - 10.1007/978-3-319-29510-7_2
DO - 10.1007/978-3-319-29510-7_2
M3 - 会议稿件
AN - SCOPUS:84958965275
SN - 9783319295091
T3 - Communications in Computer and Information Science
SP - 37
EP - 51
BT - Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
A2 - Ölveczky, Peter Csaba
A2 - Artho, Cyrille
PB - Springer Verlag
T2 - 4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
Y2 - 6 November 2015 through 7 November 2015
ER -