Matteo Camilli
ABSTRACT
Formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data coming from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the bigdata community to enable verification of very complex systems using bigdata approaches and cloud computing facilities.
- Amazon Web Services. Elastic MapReduce. http:// aws.amazon.com/documentation/elasticmapreduce/, 2013. Last visited: June 2013.Google Scholar
- J. Barnat, L. Brim, and J. Chaloupka. Parallel breadth-first search ltl model-checking. In Automated Software Engineering, 2003. Proceedings. 18th IEEE International Conference on, pages 106–115, 2003.Google ScholarCross Ref
- J. Barnat, L. Brim, and I. ˘ Cerná. Property driven distribution of nested dfs. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic, pages 1–10, Pittsburgh, PA, USA, 2002. Dept. of Electronics and Computer Science, University of Southampton.Google Scholar
- J. Barnat, L. Brim, M. ˇ Ceˇ ska, and P. Roˇ ckai. Divine: Parallel distributed model checker. In Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop on, and High Performance Computational Systems Biology, Second International Workshop on, pages 4–7, 2010. Google ScholarDigital Library
- A. Bell and B. R. Haverkort. Sequential and distributed model checking of petri nets. International Journal on Software Tools for Technology Transfer, 7(1):43–60, 2005. Google ScholarDigital Library
- C. Bellettini, M. Camilli, L. Capra, and M. Monga. Symbolic state space exploration of RT systems in the cloud. In Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, pages 295–302, Los Alamitos, CA, USA, 2012. IEEE CS Press. Google ScholarDigital Library
- C. Bellettini, M. Camilli, L. Capra, and M. Monga. Distributed CTL Model Checking in the Cloud. ArXiv e-prints, Oct. 2013.Google Scholar
- C. Bellettini, M. Camilli, L. Capra, and M. Monga. Mardigras: Simplified building of reachability graphs on large clusters. In P. Abdulla and I. Potapov, editors, Reachability Problems, volume 8169 of LNCS, pages 83–95. Springer Berlin Heidelberg, 2013.Google Scholar
- M. C. Boukala and L. Petrucci. Distributed model-checking and counterexample search for CTL logic. Int. J. Crit. Comput.-Based Syst., 3(1/2):44–59, Jan. 2012. Google ScholarDigital Library
- M. Bourahla. Distributed ctl model checking. Software, IEE Proceedings -, 152(6):297–308, 2005.Google ScholarCross Ref
- M. Camilli. Petri nets state space analysis in the cloud. In Proceedings of the 2012 International Conference on Software Engineering, ICSE 2012, pages 1638–1640, Piscataway, NJ, USA, 2012. IEEE Press. Google ScholarDigital Library
- G. Ciardo. Automated parallelization of discrete state-space generation. J. Parallel Distrib. Comput., 47(2):153–167, Dec. 1997. Google ScholarDigital Library
- G. Ciardo, J. Gluckman, and D. Nicol. Distributed state space generation of discrete-state stochastic models. INFORMS J. on Comp., 10(1):82–93, Jan. 1998. Google ScholarDigital Library
- E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999. Google ScholarDigital Library
- J. Dean and S. Ghemawat. MapReduce: simplified data processing on large clusters. Commun. ACM, 51:107–113, January 2008. Google ScholarDigital Library
- C. Eisner and D. Peled. Comparing symbolic and explicit model checking of a software system. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software, pages 230–239, London, UK, UK, 2002. Springer-Verlag. Google ScholarDigital Library
- J. Ekanayake, H. Li, B. Zhang, T. Gunarathne, S.-H. Bae, J. Qiu, and G. Fox. Twister: a runtime for iterative MapReduce. In Proc. of Symp. on High Performance Distributed Computing, pages 810–818, 2010. Google ScholarDigital Library
- S. Evangelista, L. Petrucci, and S. Youcef. Parallel nested depth-first searches for ltl model checking. In T. Bultan and P.-A. Hsiung, editors, Automated Technology for Verification and Analysis, volume 6996 of LNCS, pages 381–396. Springer Berlin Heidelberg, 2011. Google ScholarDigital Library
- R. Jhala and R. Majumdar. Software model checking. ACM Comput. Surv., 41(4):21:1–21:54, Oct. 2009. Google ScholarDigital Library
- F. Kordon et al. Web report on the model checking contest @ petri net 2013, available at http://mcc.lip6.fr, June 2013.Google Scholar
- F. Lerda and R. Sisto. Distributed-memory model checking with spin. In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pages 22–39, London, UK, UK, 1999. Springer-Verlag. Google ScholarDigital Library
- J. Lin and M. Schatz. Design patterns for efficient graph algorithms in mapreduce. In Mining and Learning with Graphs, pages 78–85, New York, 2010. ACM Press. Google ScholarDigital Library
- U. Stern and D. Dill. Parallelizing the mur¨I¸ T verifier. Formal Methods in System Design, 18(2):117–129, 2001. Google ScholarDigital Library
- C. t. Chu, S. K. Kim, Y. a. Lin, Y. Yu, G. R. Bradski, A. Y. Ng, and K. Olukotun. Map-Reduce for Machine Learning on Multicore. In Neural Information Processing Systems, pages 281–288, 2006.Google Scholar
- A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.Google ScholarCross Ref
- The Apache Software Foundation. Hadoop MapReduce. http://hadoop.apache.org/mapreduce/, 2007. Last visited: June 2013.Google Scholar
- A. Valmari. The state explosion problem. In Lectures on Petri Nets I, pages 429–528, London, UK, 1998. Springer-Verlag.Google Scholar
Index Terms
- Formal verification problems in a big data world: towards a mighty synergy
Recommendations
Challenges for MapReduce in Big Data
SERVICES '14: Proceedings of the 2014 IEEE World Congress on ServicesIn the Big Data community, MapReduce has been seen as one of the key enabling approaches for meeting continuously increasing demands on computing resources imposed by massive data sets. The reason for this is the high scalability of the MapReduce ...
Disease Surveillance System for Big Climate Data Processing and Dengue Transmission
Ambient intelligence is an emerging platform that provides advances in sensors and sensor networks, pervasive computing, and artificial intelligence to capture the real time climate data. This result continuously generates several exabytes of ...
Big Data Processing Technology Research and Application Prospects
IMCCC '14: Proceedings of the 2014 Fourth International Conference on Instrumentation and Measurement, Computer, Communication and ControlWith the rapid development of cloud computing, Internet of Things, Mobile Internet and other related technologies, data is growing at an unprecedented rate in both scales and types. Nowadays, data has been a kind of enormous business resources in the ...
Comments