Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Agesen, O., Detlefs, D., Garthwaite, A., Knippel, R., Ramakrishna, Y., White, D.: An Efficient Meta-Lock for Implementing Ubiquitous Synchronization. In: OOPSLA 1999, pp. 207–222 (1999)
Agrawal, H., Horgan, J., London, S., Wong, W.: Fault localization using execution slices and dataflow tests. In: ISSRE 1995, pp. 143–151 (1995)
Brookes, S.D., Roscoe, A.W., Walker, D.J.: An Operational Semantics for CSP. Technical report (1986)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control 52(5), 782–798 (2005)
Herlihy, M., Wing, J.M.: Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. on Prog. Lang. and Syst (TOPLAS) 12(3), 463–492 (1990)
Horwitz, S.: Identifying the semantic and textual differences between two versions of a program. SIGPLAN Not. 25(6), 234–245 (1990)
Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)
Jackson, D., Ladd, D.: Semantic diff: A tool for summarizing the effects of modifications. In: ICSM 1994, pp. 243–252 (1994)
Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-Based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007)
Jones, J., Harrold, M.: Empirical evaluation of the tarantula automatic fault-localization technique. In: ASE 2005, pp. 273–282 (2005)
Könighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: FMCAD 2009, pp. 152–159 (2009)
Liu, Y., Sun, J., Dong, J.S.: An Analyzer for Extended Compositional Process Algebras. In: ICSE 2008 Companion, pp. 919–920 (2008)
Masri, W.: Fault localization based on information flow coverage. Technical report, AUB-CMPS-07-10 (2007)
Mayer, W., Stumptner, M.: Model-based debugging – state of the art and future challenges. Electron. Notes Theor. Comput. Sci. 174(4), 61–82 (2007)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Operational and algebraic semantics of concurrent processes, pp. 1201–1242 (1990)
Nejati, S., Sabetzadeh, M., Chechik, M., Easterbrook, S., Zave, P.: Matching and merging of statecharts specifications. In: ICSE 2007, pp. 54–64 (2007)
Sokolsky, S.K.O., Lee, I.: Simulation-based graph similarity. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 426–440. Springer, Heidelberg (2006)
Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: Nyberg, K. (ed.) FSE 2008. LNCS, vol. 5086, pp. 226–237. Springer, Heidelberg (2008)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, ∞ )-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)
Qi, D., Roychouhury, A., Liang, Z., Vaswani, K.: Darwin: an approach for debugging evolving programs. In: Dunkelman, O. (ed.) FSE 2009. LNCS, vol. 5665, pp. 33–42. Springer, Heidelberg (2009)
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: ISSTA 2006, pp. 157–168 (2006)
Sun, J., Liu, Y., Dong, J.S., Chen, C.Q.: Integrating Specification and Programs for System Modeling and Verification. In: TASE 2009, pp. 127–135 (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Treiber, R.K.: Systems Programming: Coping with Parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)
Valmari, A.: Stubborn Set Methods for Process Algebras. In: PMIV 1996, pp. 213–231 (1996)
Xing, Z.: Genericdiff: A general framework for model comparison. Technical report, National University of Singpore (2011), http://www.comp.nus.edu.sg/~pat/publications/gendiff.pdf
Yang, W.: Identifying syntactic differences between two programs. Softw. Pract. Exper. 21(7), 739–755 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xing, Z., Sun, J., Liu, Y., Dong, J.S. (2011). Differencing Labeled Transition Systems. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)