Differencing labeled transition systems

Concurrent programs often use Labeled Transition Systems (LTSs) as their operational semantic models, which provide the basis for automatic system analysis and verification. System behaviors (generated from the operational semantics) evolve as programs evolve for fixing bugs or implementing new user...

Full description

Saved in:
Bibliographic Details
Main Authors: XING, Zhenchang, SUN, Jun, LIU, Yang, DONG, Jin Song
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2011
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/5031
https://ink.library.smu.edu.sg/context/sis_research/article/6034/viewcontent/Differencing_Labeled.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-6034
record_format dspace
spelling sg-smu-ink.sis_research-60342020-03-12T08:38:37Z Differencing labeled transition systems XING, Zhenchang SUN, Jun LIU, Yang DONG, Jin Song Concurrent programs often use Labeled Transition Systems (LTSs) as their operational semantic models, which provide the basis for automatic system analysis and verification. System behaviors (generated from the operational semantics) evolve as programs evolve for fixing bugs or implementing new user requirements. Even when a program remains unchanged, its LTS models explored by a model checker or analyzer may be different due to the application of different exploration methods. In this paper, we introduce a novel approach (named SpecDiff) to computing the differences between two LTSs, representing the evolving behaviors of a concurrent program. SpecDiff considers LTSs as Typed Attributed Graphs (TAGs), in which states and transitions are encoded in finite dimensional vector spaces. It then computes a maximum common subgraph of two TAGs, which represents an optimal matching of states and transitions between two evolving LTSs of the concurrent program. SpecDiff has been implemented in our home grown model checker framework PAT. Our evaluation demonstrates that SpecDiff can assist in debugging system faults, understanding the impacts of state reduction techniques, and revealing system change patterns. 2011-10-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5031 info:doi/10.1007/978-3-642-24559-6_36 https://ink.library.smu.edu.sg/context/sis_research/article/6034/viewcontent/Differencing_Labeled.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Checker Operational Semantic Label Transition System Concurrent Program Symbolic Execution Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Model Checker
Operational Semantic
Label Transition System
Concurrent Program
Symbolic Execution
Software Engineering
spellingShingle Model Checker
Operational Semantic
Label Transition System
Concurrent Program
Symbolic Execution
Software Engineering
XING, Zhenchang
SUN, Jun
LIU, Yang
DONG, Jin Song
Differencing labeled transition systems
description Concurrent programs often use Labeled Transition Systems (LTSs) as their operational semantic models, which provide the basis for automatic system analysis and verification. System behaviors (generated from the operational semantics) evolve as programs evolve for fixing bugs or implementing new user requirements. Even when a program remains unchanged, its LTS models explored by a model checker or analyzer may be different due to the application of different exploration methods. In this paper, we introduce a novel approach (named SpecDiff) to computing the differences between two LTSs, representing the evolving behaviors of a concurrent program. SpecDiff considers LTSs as Typed Attributed Graphs (TAGs), in which states and transitions are encoded in finite dimensional vector spaces. It then computes a maximum common subgraph of two TAGs, which represents an optimal matching of states and transitions between two evolving LTSs of the concurrent program. SpecDiff has been implemented in our home grown model checker framework PAT. Our evaluation demonstrates that SpecDiff can assist in debugging system faults, understanding the impacts of state reduction techniques, and revealing system change patterns.
format text
author XING, Zhenchang
SUN, Jun
LIU, Yang
DONG, Jin Song
author_facet XING, Zhenchang
SUN, Jun
LIU, Yang
DONG, Jin Song
author_sort XING, Zhenchang
title Differencing labeled transition systems
title_short Differencing labeled transition systems
title_full Differencing labeled transition systems
title_fullStr Differencing labeled transition systems
title_full_unstemmed Differencing labeled transition systems
title_sort differencing labeled transition systems
publisher Institutional Knowledge at Singapore Management University
publishDate 2011
url https://ink.library.smu.edu.sg/sis_research/5031
https://ink.library.smu.edu.sg/context/sis_research/article/6034/viewcontent/Differencing_Labeled.pdf
_version_ 1770575194187890688