An efficient approach to state space management in model checking of complex software systems using machine learning techniques

Abstract

Since complexity of computer systems is growing increasingly, assuring flawless operation of these systems has become more difficult. Therefore, it is important that these systems whether software or hardware are executed as expected. Consequently, verifying system before implementation at model level is necessary. Model checking is a formal technique for validating the system automatically which decides whether the finite state system satisfies temporal property by scanning the whole state space or not. One of the most important problems in model checking is state space explosion of models which results in memory shortage in generation of all states. Therefore, this paper presents a method which employs machine learning techniques without exploring the whole state space to predict temporal properties of trajectories in systems based on graph transmission system. the proposed method is implemented in Groove; results indicate desirable accuracy and speed of this method compared to other methods.

Get full access to this article

View all access options for this article.

References

Abowd ,

Allen and

Garlan , Using style to give meaning to softwarearchitecture, ACM SIGSOFT Software Engineering Notes, ACM 18(5) (1993), 9–20.

Garlan ,

Allen and

Ockerbloom , Exploiting style in architectural designenvironments, ACM SIGSOFT Software Engineering Notes, ACM 19(5) (1994), 175–188.

Thöne , Dynamic software architectures: a style based modeling andrefinement technique with graph transformations, in: Ph.D. Thesis, Faculty of Computer Science, Electrical Engineering and Mathematics, University of Paderborn, Paderborn, Germany, 2005.

J.H.

Hausmann , Dynamic Meta Modeling: A Semantics Description Techniquefor Visual Modeling Techniques, Universität Paderborn, Paderborn, Germany, 2005.

Baier ,

J.P.

Katoen and

K.G.

Larsen , Principles of Model Checking, vol. 2620264, MIT Press, Cambridge, 2008.

C.S.

Jensen ,

Møller ,

Raychev ,

Dimitrov and

Vechev , Stateless modelchecking of event-driven applications, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems Languages, and Applications. ACM (2015) 57–73.

E.M.

Clarke ,

K.L.

McMillan ,

S.V.A.

Campos and

V.i.

Hartonas-Garmhausen , Symbolic model checking, Comput. Aided Verif. 1102 (1996), 419–422.

J.R.

Burch ,

E.M.

Clarke ,

K.L.

McMillan ,

D.L.

Dill and

L.J.

Hwang , Symbolic model checking: 1020 states and beyond, Inform. Comput. 98 (1992), 142–170.

Edelkamp ,

Leue and

A.L.

Lafuente , Directed explicit-state model checking inthe validation of communication protocols, Int. J. Software Tools Technol. (STTT) 5(2--3) (2004), 247–267.

10.

Bošnački ,

Leue and

A.L.

Lafuente , Partial-order reduction for general state exploring algorithms, Int. J. Softw. Tools Technol. Transf. (STTT) 11 (2009), 39–51.

11.

A.L.

Lafuente , Symmetry reduction and heuristic search for error detection inmodel checking, Workshop on Model Checking and Artificial Intelligence (2003).

12.

E.A.

Emerson and

A.P.

Sistla , Symmetry and model checking, Formal Methods Syst. Des. 9(1996) 105–131 (Special issue on symmetry in automatic verification).

13.

E.M.

Clarke ,

Enders ,

Filkorn and

Jha , Exploiting symmetry in temporal logic model checking, Formal Methods Syst. Des. 9 (1996), 77–104 (Special issue on symmetry in automatic verification).

14.

Gyuris ,

A.P.

Sistla , On-the-fly model checking under fairness that exploits symmetry, Formal Methods Syst. Des. 15 (1999), 217–238.

15.

Rafe , Scenario-driven analysis of systems specified through graphtransformations, J. Visual Lang. Comput. 24(2)(2013), 136–145.

16.

Pira ,

Rafe and

Nikanjam , EMCDM: Efficient model checking by data mining for verification ofcomplex software systems specified through architectural styles, J. Applied Soft Computing V49 (2016), 1185–1201.

17.

Agrawal and

Srikant , Fast algorithms for mining association rules, Proceedings of the 20th VLDB Conference (1994), 487–499.

18.

Han ,

Pei and

Yin , Mining frequent patterns without candidate generation, Proceedings of ACM SIGMOD International Conference on Management of Data (2000)pp 1–12.

19.

Zaki ,

Parthasarathy ,

Ogihara and

Li , New algorithms for fast discoveryof association rules, KDD 97 (1997), 283–286.

20.

Pira ,

Rafe and

Nikanjam , Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations, Information and Software Technology 97 (2018), 110–134.

21.

Yousefian ,

Rafe and

Rahmani , A heuristic approach for model checking graph transformation systems, Appl. Soft Comput. 24 (2014), 169–180.

22.

Francesca ,

Santone ,

Vaglini and

M.L.

Villani , Ant colony optimization fordeadlock detection in concurrent systems, Computer Software and Applications Conference (COMPSAC), IEEE (2011), 108–117.

23.

Alba and

Chicano , Finding safety errors with ACO, Proceedings of the 9th Annual Conference on Genetic and Evolutionary Computation, ACM (2007), 1066–1073.

24.

Rafe ,

Darghayedi and

Pira , MS-ACO: A multi-stage ant colony optimization to refute complex software systems specified through graph transformation, Soft Comput. (2019), 4531–4556.

25.

Rafe ,

Moradi ,

Yousefian and

Nikanjam , A meta-heuristic approach for automated refutation of complex software systems specified through graph transformations, Appl. Soft Comput. 33 (2015), 136–149.

26.

Pira ,

Rafe and

Nikanjam , Using evolutionary algorithms for reach ability analysis of complex software systems specified through graph transformation, Reliability Engineering & System Safety 191 (2019), 106577.

27.

Partabian ,

Rafe ,

Parvin and

Nejatian , An approach based on knowledge exploration for state space management in checking reach ability of complex software systems, Soft Comput. (2019), pp 1–16.

28.

Baresi and

Heckel , Tutorial introduction to graph transformation: A software engineering perspective, in: First International Conference on Graph Transformation (ICGT), 2002, pp. 402–429.

29.

Ehrig ,

Prange and

Taentzer , Fundamentals of Algebraic Graph Transformation, in: EATCS Monographs in TCS, Springer, Heidelberg, 2006.

30.

Rozenberg , Handbook of Graph Grammars and Computing by Graph Transformation: Applications, vol. 1, World scientific, Singapore, 1997.

31.

32.

Ehrig ,

Engels ,

H.J.

Kreowski and

Rozenberg , Handbook of graph grammars and computing by graph transformation: Applications, Lang. Tools (1999).

33.

Ehrig ,

Pfender and

H.J.

Schneider , Graph-Grammars: An Algebraic Approach, in: Proceeding SWAT ‘73 Proceedings of the 14th Annual Symposium on Switching and Automata Theory, IEEE Computer Society, Swat 1973, pp. 167–180.

34.

Heckel , Compositional verification of reactive systems specified by graph transformation, Fundament. Approaches Softw. Eng. (FASE) 1382 (1998), 138–153.

35.

Vapnik , Statistical Learning Theory. Wiley, (1998).

36.

Vapnik and

Chapelle , Bounds on error expectation for support vector machines, Neural Computation 12(9), 2000.

37.

B.E.

Boser ,

I.M.

Guyon and

V.N.

Vapnik , A training algorithm for optimal margin classifiers. In

Haussler , editor, 5th Annual ACM Workshop on COLT, pages 144–152, Pittsburgh, PA, 1992. ACM Press.

38.

Kastenberg and

Rensink , Model checking dynamic states in GROOVE, in: 13th International Conference on Model Checking Software, Springer-Verlag, Berlin, Heidelberg, 2006, pp. 299–305.

39.

Rensink ,

Boneva ,

Kastenberg and

Staijen , User manual for the GROOVE tool set, 2010, Available from: http://groove.cs.utwente.nl/wp-content/uploads/usermanual1.pdf

40.

Tom M.

Mitchell , Machine Learning. WCB/McGraw-Hill, 1997.

41.

Pattern Recognition and Machine Learning,

Christopher M.

Bishop , 2006.

42.

R.S.

Sutton and

A.G.

Barto , Reinforcement Learning: An Introduction, 1998.

43.

Introduction to machine learning,

Nils J.

Nilson , 1997.

44.

T.G.

Dietterich , An experimental comparison of three methods for constructing ensembles of decision trees: Bagging, boosting, and randomization, Machine Learning 40 (2000), 139–157.

45.

E.A.

Emerson and

A.P.

Sistla , Symmetry and model checking, Formal Methods Syst. Des. 9 (1996) 105–131 (Special issue on symmetry in automatic verification).

46.

E.M.

Clarke ,

Enders ,

Filkorn and

Jha , Exploiting symmetry in temporal logic model checking, Formal Methods Syst. Des. 9 (1996) 77–104 (Special issue on symmetry in automatic verification).

47.

Gyuris and

A.P.

Sistla , On-the-fly model checking under fairness that exploits symmetry, Formal Methods Syst. Des. 15 (1999), 217–238.

48.

Courcoubetis ,

Vardi ,

Wolper and

Yannakakis , Memory efficient algorithms for the verification of temporal properties, Formal Methods Syst. Des. 1 (1992) 275–288 (Special issue on computer-aided verification).

49.

Stern and

D.L.

Dill , Improved probabilistic verification by hash compaction, in: IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Springer-Verlag, London, UK, 1995, pp. 206–224.

50.

Stern and

D.L.

Dill , A new scheme for memory-efficient probabilistic verification, in: On Formal Description Techniques IX/Protocol Specification, Testing and Verification XVI on Formal Description Techniques IX: Theory, Application and Tools: Theory, Application and Tools, Chapman & Hall, Ltd., London, UK, 1996, pp. 333–348.

51.

Wolper and

Leroy , Reliable hashing without collision detection, in: Computer Aided Verification, 5th International Conference, 1993, pp. 59–70.

52.

Sivaraj and

Gopalakrishnan , Random walk based heuristic algorithms for distributed memory model checking, Electron. Notes Theor. Comput. Sci. (ENTCS) 89 (2003), 51–67.

53.

F.J.

Lin ,

P.M.

Chu and

M.T.

Liu , Protocol verification using reach ability analysis: the state space explosion problem and relief strategies, in: ACM Workshop on Frontiers in Computer Communications Technology, 1987, pp. 126–135.

54.

Edelkamp and

Reffel , OBDDs in Heuristic Search, in: KI, volume 1504 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 81–92.

55.

Stefan and

M.T.

Befrouei , “Mining sequential patterns to explain concurrent counterexamples”. Springer Berlin Heidelberg, 2013.

56.

Gaschnig , Performance measurement and analysis of certain search algorithms, in: PhD Thesis, Carnegie-Mellon University, Pittsburg, 1979.

57.

C.H.

Yang and

D.L.

Dill , Validation with guided search of the state space, in: DAC’98 Proceedings of the 35th Annual Design Automation Conference, 1998, pp. 599–604.

58.

Godefroid and

Khurshid , Exploring very large state spaces using geneticalgorithms, in: Tools and Algorithms for the Construction and Analysis ofSystems, Springer, Berlin, Germany, 2002, pp. 266–280.

59.

Behjati ,

Sirjani and

M.N.

Ahmadabadi , Bounded rational search for on-thefly model checking of LTL properties, in: Third IPM International Conference on Fundamentals of Software Engineering, Springer-Verlag Berlin, Heidelberg, 2010, pp. 292–307.

60.

Ge ,

Pantel and

Crégut , Automated failure analysis in model checkingbased on data mining, in: Model and Data Engineering, Springer International Publishing, New York, USA, 2014, pp. 13–28.

61.

Sidorov,

Grigori ;

Velazquez,

Francisco ;

Stamatatos,

Efstathios ;

Gelbukh,

Alexander and

Chanona-Hernández,

Liliana , “Syntactic Dependency-based n-grams as Classification Features”. LNAI 7630 (2012), 1–11.

62.

Sidorov,

Grigori , “Syntactic Dependency-Based n-grams in Rule Based Automatic English as Second Language Grammar Correction”, International Journal of Computational Linguistics and Applications 4(2) (2013), 169–188.

63.

Sidorov,

Grigori ;

Velasquez,

Francisco ;

Stamatatos,

Efstathios ;

Gelbukh,

Alexander ;

Chanona-Hernández,

Liliana . “Syntactic n-Grams as Machine Learning Features for Natural Language Processing”. Expert Systems with Applications 41(3)(XXXX), 853–860. doi:10.1016/j.eswa.2013.08.015

64.

Lioma ,

C.J.K.

van Rijsbergen , “Part of Speech n-Grams and Information Retrieval” (PDF). French Review of Applied Linguistics, Special issue on Information Extraction and Linguistics XIII(2008/1) (2008), Cairn 9–22.

65.

Z.-H.

Zhou , Ensemble Methods: Foundations and Algorithms, Chapman & Hall/CRC (2012).