MapReduce for Parallel Trace Validation of LTL Properties
作者： Benjamin Barre , Mathieu Klein , Maxime Soucy-Boivin , Pierre-Antoine Ollivier , Sylvain Hallé
DOI: 10.1007/978-3-642-35632-2_20
关键词: Cloud computing 、 Process (computing) 、 Computer science 、 Linear temporal logic 、 Propositional variable 、 Event (computing) 、 Parallel computing 、 Temporal logic 、 TRACE (psycholinguistics)
摘要: We present an algorithm for the automated verification of Linear Temporal Logic formulae on event traces using increasingly popular cloud computing framework called MapReduce. The can process multiple, arbitrary fragments trace in parallel, and compute its final result through a cycle runs MapReduce instances. Compared to classical, single-instance solutions, proof-of-concept implementation shows experimental evaluation how reduces by as much 90% number operations that must be performed linearly, resulting commensurate speed gain.
springer.com
researchgate.net 
sci-hub.st 参考文章(28)
A. Pnueli, A. Zaks, On the Merits of Temporal Testers 25 Years of Model Checking. pp. 172- 195 ,(2008) , 10.1007/978-3-540-69850-0_11
W.M.P. van der Aalst, M. Pesic, Specifying and Monitoring Service Flows: Making Web Services Process-Aware Test and analysis of web services. pp. 11- 55 ,(2007) , 10.1007/978-3-540-72912-9_2
Hubert Garavel, Radu Mateescu, SEQ.OPEN: A tool for efficient trace-based verification international workshop on model checking software. pp. 151- 157 ,(2004) , 10.1007/978-3-540-24732-6_11
Lars Kuhtz, Bernd Finkbeiner, LTL Path Checking Is Efficiently Parallelizable Automata, Languages and Programming. pp. 235- 246 ,(2009) , 10.1007/978-3-642-02930-1_20
Prasad Naldurg, Koushik Sen, Prasanna Thati, A Temporal Logic Based Framework for Intrusion Detection formal techniques for networked and distributed systems. pp. 359- 376 ,(2004) , 10.1007/978-3-540-30232-2_23
David Basin, Felix Klaedtke, Samuel Müller, Policy monitoring in first-order temporal logic computer aided verification. pp. 1- 18 ,(2010) , 10.1007/978-3-642-14295-6_1
Sylvain Hallé, Roger Villemaire, XML Methods for Validation of Temporal Properties on Message Traces with Data OTM '08 Proceedings of the OTM 2008 Confederated International Conferences, CoopIS, DOA, GADA, IS, and ODBASE 2008. Part I on On the Move to Meaningful Internet Systems:. pp. 337- 353 ,(2008) , 10.1007/978-3-540-88871-0_23
Michael H. Böhlen, Jan Chomicki, Richard T. Snodgrass, David Toman, Querying TSQL2 databases with temporal logic Advances in Database Technology — EDBT '96. pp. 325- 341 ,(1996) , 10.1007/BFB0014161
Rajeev Motwani, Terry Winograd, Lawrence Page, Sergey Brin, The PageRank Citation Ranking : Bringing Order to the Web the web conference. ,vol. 98, pp. 161- 172 ,(1999)
Yeonhee Lee, Wonchul Kang, Youngseok Lee, A hadoop-based packet trace processing tool traffic monitoring and analysis. pp. 51- 63 ,(2011) , 10.1007/978-3-642-20305-3_5