Active automata learning is a promising technique to generate formal behavioral models of systems by experimentation. The practical applicability of active learning, however, is often hampered by the impossibility of realizing so-called equivalence queries, which are vital for ensuring progress during learning and finally resulting in correct models.
This paper discusses the proposed approach of using monitoring as a means of generating counterexamples, explains in detail why virtually all existing learning algorithms are not suited for this approach, and gives an intuitive account of TTT, an algorithm designed to cope with counterexamples of extreme length. The essential steps and the impact of TTT are illustrated via experimentation with LearnLib, a free, open source Java library for active automata learning.
Philip Daian, Runtime Verification Inc., USA
Yliès Falcone, University of Grenoble I, France
Patric Meredith, Runtime Verification Inc., USA
Traian Florin Serbanuta, Runtime Verification Inc., USA
Shin’ichi Shiriashi, Denso International America Inc., USA
Akihito Iwai, Toyota InfoTechnology Center, USA
Grigore Rosu, University of Illinois at Urbana-Champaign, USA
RV-Android is a new freely available proprietary runtime library for monitoring formal safety properties on Android. RV-Android uses RV-Monitor as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitor- ing work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption, efficiency, and battery life considerations. We demonstrate the developer usage of RV- Android with the standard Android build process, using instrumentation mechanisms effective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expressiveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.
Dejan Nickovic, Austrian Institute of Technology, Austria
Continuous and hybrid behaviors naturally arise from various dynamical systems. In this tutorial, we present state-of-the-art techniques for qualitative and quantitative reasoning about such behaviors. We introduce Signal Temporal Logic and Timed Regular Expressions as specification languages that we use to describe properties of hybrid systems. We then provide an overview of methods for (1) checking whether a hybrid behavior is correct and robust with respect to its specification; and (2) measuring of quantitative characteristics of a hybrid system by property-driven extraction of relevant data from its behaviors. We introduce the tools that support such analysis and discuss their application in several application domains.
Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.