Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines

Clemens Dubslaff; Patrick Wienhöft; Ansgar Fehnker

doi:10.1007/978-3-030-92124-8_19

Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines

Clemens Dubslaff^*, Patrick Wienhöft, Ansgar Fehnker

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

62 Downloads (Pure)

Abstract

Recursive state machines (RSMs) are state-based models for
procedural programs with wide-ranging applications in program verification
and interprocedural analysis. Model-checking algorithms for RSMs and related
formalisms and various temporal logic specifications
have been intensively studied in the literature.

In this paper, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL)} that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analysed in those cases in which it might influence the satisfaction of the CTL requirement.

We evaluate our prototypical implementation on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison to
state-of-the-art model-checking tools for procedural programs.

Original language	English
Title of host publication	Software Engineering and Formal Methods
Subtitle of host publication	19th International Conference
Publisher	Springer
Pages	332-350
DOIs	https://doi.org/10.1007/978-3-030-92124-8_19
Publication status	Published - 6 Dec 2021
Event	19th International Conference on Software Engineering and Formal Methods, SEFM 2021 - Virtual Conference Duration: 6 Dec 2021 → 10 Dec 2021 Conference number: 19

Conference

Conference	19th International Conference on Software Engineering and Formal Methods, SEFM 2021
Abbreviated title	SEFM 2021
City	Virtual Conference
Period	6/12/21 → 10/12/21

Keywords

Model Checking
recursive state machines
Lazy Evaluation

Access to Document

10.1007/978-3-030-92124-8_19

mainAccepted author version, 701 KB

Cite this

@inproceedings{15127c0e2afb4b6a97b4acf4b31eb220,

title = "Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines",

abstract = "Recursive state machines (RSMs) are state-based models forprocedural programs with wide-ranging applications in program verificationand interprocedural analysis. Model-checking algorithms for RSMs and relatedformalisms and various temporal logic specificationshave been intensively studied in the literature.In this paper, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL)} that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analysed in those cases in which it might influence the satisfaction of the CTL requirement.We evaluate our prototypical implementation on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison tostate-of-the-art model-checking tools for procedural programs.",

keywords = "Model Checking, recursive state machines, Lazy Evaluation",

author = "Clemens Dubslaff and Patrick Wienh{\"o}ft and Ansgar Fehnker",

year = "2021",

month = dec,

day = "6",

doi = "10.1007/978-3-030-92124-8_19",

language = "English",

pages = "332--350",

booktitle = "Software Engineering and Formal Methods",

publisher = "Springer",

note = "19th International Conference on Software Engineering and Formal Methods, SEFM 2021, SEFM 2021 ; Conference date: 06-12-2021 Through 10-12-2021",

}

Dubslaff, C, Wienhöft, P & Fehnker, A 2021, Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines. in Software Engineering and Formal Methods: 19th International Conference. Springer, pp. 332-350, 19th International Conference on Software Engineering and Formal Methods, SEFM 2021, Virtual Conference, 6/12/21. https://doi.org/10.1007/978-3-030-92124-8_19

TY - GEN

T1 - Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines

AU - Dubslaff, Clemens

AU - Wienhöft, Patrick

AU - Fehnker, Ansgar

N1 - Conference code: 19

PY - 2021/12/6

Y1 - 2021/12/6

N2 - Recursive state machines (RSMs) are state-based models forprocedural programs with wide-ranging applications in program verificationand interprocedural analysis. Model-checking algorithms for RSMs and relatedformalisms and various temporal logic specificationshave been intensively studied in the literature.In this paper, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL)} that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analysed in those cases in which it might influence the satisfaction of the CTL requirement.We evaluate our prototypical implementation on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison tostate-of-the-art model-checking tools for procedural programs.

AB - Recursive state machines (RSMs) are state-based models forprocedural programs with wide-ranging applications in program verificationand interprocedural analysis. Model-checking algorithms for RSMs and relatedformalisms and various temporal logic specificationshave been intensively studied in the literature.In this paper, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL)} that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analysed in those cases in which it might influence the satisfaction of the CTL requirement.We evaluate our prototypical implementation on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison tostate-of-the-art model-checking tools for procedural programs.

KW - Model Checking

KW - recursive state machines

KW - Lazy Evaluation

U2 - 10.1007/978-3-030-92124-8_19

DO - 10.1007/978-3-030-92124-8_19

M3 - Conference contribution

SP - 332

EP - 350

BT - Software Engineering and Formal Methods

PB - Springer

T2 - 19th International Conference on Software Engineering and Formal Methods, SEFM 2021

Y2 - 6 December 2021 through 10 December 2021

ER -

Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this