Skip to main content
SpringerLink
Log in

Direct Model Checking Matrix Algorithm

  • Short Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

During the last decade, Model Checking has proven its efficacy and power in circuit design, network protocol analysis and bug hunting. Recent research on automatic verification has shown that no single model-checking technique has the edge over all others in all application areas. So, it is very difficult to determine which technique is the most suitable for a given model. It is thus sensible to apply different techniques to the same model. However, this is a very tedious and time-consuming task, for each algorithm uses its own description language. Applying Model Checking in software design and verification has been proved very difficult. Software architectures (SA) are engineering artifacts that provide high-level and abstract descriptions of complex software systems. In this paper a Direct Model Checking (DMC) method based on Kripke Structure and Matrix Algorithm is provided. Combined and integrated with domain specific software architecture description languages (ADLs), DMC can be used for computing consistency and other critical properties.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time. Acta Information, 1983, 20(3): 207–226.

    Article  MathSciNet  Google Scholar 

  2. Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. Annuanl ACM IEEE Design Automation Conference, New Orleans, USA, 1999, pp.317–320.

  3. Biere A, Cimatti A, Clarek E, Zhu Y. Symbolic model checking without BDDs. In Proc. the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS, Springer-Verlag, 1999, 1579: 193–207.

  4. Burch J R, Clarke E M, McMillan K L. Symbolic model checking: 1020 states and beyond. Information and Computation, 1992, 98(2): 142–170.

    Article  MathSciNet  Google Scholar 

  5. Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs: Workshop, Yorktoen Heights, LNCS, NY: Springer, 1981, 131: 52–71.

  6. Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244–263.

    Article  Google Scholar 

  7. Aho A V, Hopcroft J E, Ullman J D. The Design and Analysis of Computer Algorithms. Addison Wesley, 1974.

  8. McMillan K L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.

  9. Holzmann G. The Spin model checker. IEEE Trans. Software Engineering, May 1999, 23(5): 279–295.

    Article  Google Scholar 

  10. Liu Jian, Lin Hui-Min. Consistency between the predicate μ-calculus and modal graphs. Journal of Software, 2003, 14(10): 1672–1680.

    MathSciNet  Google Scholar 

  11. Zhu X Y, Tang Z S. A temporal logic-based software architecture description language XYZ/ADL. Journal of Software, 2003, 14(4): 713–720.

    MathSciNet  Google Scholar 

  12. Bjesse P, Leonard T, Mokkedem A. Finding bugs in an alpha microprocessor using satisfiability solvers. In Proc. 13th Int. Conf. Computer Aided Verification (CAV’01), Berry G, Comon H, Finkel A (eds.), Lecture Notes in Computer Science, Springer-Verlag, 2001, 2102: 454–464.

  13. Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA: The MIT Press, 2000.

    Google Scholar 

  14. Allen R, Garlan D. A formal basis for architectural connection. ACM Trans. Software Engineering and Methodology, July 1997, 6(3): 213–249.

    Article  Google Scholar 

  15. ITU-T Z 100–2000. Specification and description language, Dec 2000.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Technology, Peking University, Beijing, 100871, P.R. China

    Zhi-Hong Tao & Li-Fu Wang

  2. Department of Computer Science, Paderborn University, D-33095, Germany

    Hans Kleine Büning

Authors
  1. Zhi-Hong Tao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hans Kleine Büning
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Li-Fu Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhi-Hong Tao.

Additional information

Supported by the National High-Tech Development 863 Program of China under Grant No.~2001AA113171 and the National Basic Research 973 Program of China under Grant No. 2002CB312006.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Tao, ZH., Büning, H.K. & Wang, LF. Direct Model Checking Matrix Algorithm. J Comput Sci Technol 21, 944–949 (2006). https://doi.org/10.1007/s11390-006-0944-5

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-006-0944-5

Keywords

Search

Navigation