RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction)
This paper introduces the RV-TOP track at ISoLA’18. The purpose of the track is to bring together experts on runtime verification and industry practitioners domains to (i) disseminate advanced research topics (ii) disseminate current industrial challenges
- PDF / 192,950 Bytes
- 6 Pages / 439.37 x 666.142 pts Page_size
- 12 Downloads / 167 Views
2
Vienna University of Technology, Vienna, Austria [email protected] Univ. Grenoble Alpes, CNRS, Inria, LIG, 38000 Grenoble, France
Abstract. This paper introduces the RV-TOP track at ISoLA’18. The purpose of the track is to bring together experts on runtime verification and industry practitioners domains to (i) disseminate advanced research topics (ii) disseminate current industrial challenges and (iii) get RV more attractive to industry and usable in additional application domains. The track consists of eight contributed papers presented during three sessions.
1
Introduction
Runtime Verification (RV) [6,8] has gained much focus, from both the research community and practitioners. Roughly speaking, RV combines a set of theories, techniques and tools aiming towards efficient analysis of systems’ executions and guaranteeing their correctness using monitoring techniques. Major challenges in RV include characterizing and formally expressing requirements that can be monitored, proposing intuitive and concise specification formalisms, and monitoring specifications efficiently (time and memory-wise). RV can be employed before the deployment, for testing, verification, and debugging purposes or after deployment to trigger some system recovery actions when a safety property is violated and for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. For example, one application of RV particularly studied in this track is to use it in combination with runtime enforcement. Runtime enforcement [15,17,20] is a powerful technique to ensure that a program conforms to its specification. It has been initiated with the work of Schneider on security automata which halt the program whenever it deviates from its safety specification. Since then, several models and frameworks have been defined to augment enforcement mechanisms with new primitives [10,14, 18,21,35] or allow them to enforce more expressive specifications [19,38,41]. As a field, major strides have been made recently to make RV a full fledge verification technique: – RV is now endowed with a competition for tools: three incarnations of the competition have been organized [2,22,40], an extensive report on the first c Springer Nature Switzerland AG 2018 T. Margaria and B. Steffen (Eds.): ISoLA 2018, LNCS 11247, pp. 3–8, 2018. https://doi.org/10.1007/978-3-030-03427-6_1
4
E. Bartocci and Y. Falcone
edition has been published [7], and a successful workshop reporting reflections on past competitions has been organized [39]. – A European COST action, ArVi1 , is ongoing with the purposes of (i) clarifying the dimensions of RV, its theory, algorithms and methods (ii) expose the landscape of formalisms and tools proposed and built for RV (iii) expose novel and challenging computational domains for RV and monitoring (iv) study potential applications of RV to important application areas beyond software and hardware reliability, including medical devices and legal contracts. – Two successful schools dedicated to Runt
Data Loading...
