nfer – A Notation and System for Inferring Event Stream Abstractions
作者： Sean Kauffman , Klaus Havelund , Rajeev Joshi
DOI: 10.1007/978-3-319-46982-9_15
关键词:
摘要: We propose a notation for specifying event stream abstractions use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated Curiosity rover on Mars. The approach builds hierarchy visualization and querying aid human comprehension. Such can also be used as input other runtime verification tools. inspired Allen’s Temporal Logic, provides rule-based declarative way express abstractions. system written Scala, specification language implemented an internal DSL. It based parallel executing actors communicating via publish-subscribe model. illustrate solution several examples, including real analysis scenario.
springer.com
sci-hub.st 参考文章(19)
Klaus Havelund, Rajeev Joshi, Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior international conference on formal engineering methods. pp. 187- 202 ,(2014) , 10.1007/978-3-319-11737-9_13
Ricky W. Butler, Radu I. Siminiceanu, Cesar A. Munoz, The Anmlite Language and Logic for Specifying Planning Problems ,(2013)
Klaus Havelund, Rajeev Joshi, Experience with Rule-Based Analysis of Spacecraft Logs international workshop formal techniques for safety-critical systems. pp. 1- 16 ,(2014) , 10.1007/978-3-319-17581-2_1
Michael Reichhardt Hansen, Dang Van Hung, A theory of duration calculus with application Domain modeling and the duration calculus. pp. 119- 176 ,(2007) , 10.1007/978-3-540-74964-6_3
David Basin, Matúš Harvan, Felix Klaedtke, Eugen Zălinescu, MONPOLY: monitoring usage-control policies runtime verification. pp. 360- 364 ,(2011) , 10.1007/978-3-642-29860-8_27
Radu I. Siminiceanu, Rick W. Butler, César A. Muñoz, Experimental Evaluation of a Planning Language Suitable for Formal Verification Model Checking and Artificial Intelligence. pp. 132- 146 ,(2009) , 10.1007/978-3-642-00431-5_9
Axel Legay, Benoît Delahaye, Saddek Bensalem, Statistical Model Checking: An Overview Runtime Verification. pp. 122- 135 ,(2010) , 10.1007/978-3-642-16612-9_11
Grigore Roşu, Saddek Bensalem, Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis Computer Aided Verification. pp. 263- 277 ,(2006) , 10.1007/11817963_25
Andreas Bauer, Martin Leucker, Christian Schallhart, The good, the bad, and the ugly, but how ugly is ugly? runtime verification. ,vol. 4839, pp. 126- 138 ,(2007) , 10.1007/978-3-540-77395-5_11
S. Shoham, E. Yahav, S.J. Fink, M. Pistoia, Static Specification Mining Using Automata-Based Abstractions IEEE Transactions on Software Engineering. ,vol. 34, pp. 651- 666 ,(2008) , 10.1109/TSE.2008.63