@inproceedings{6042, abstract = {Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.}, author = {Christakis, Maria and Heizmann, Matthias and Mansur, Muhammad Numair and Schilling, Christian and Wüstholz, Valentin}, booktitle = {25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems }, location = {Prague, Czech Republic}, pages = {226--243}, publisher = {Springer Nature}, title = {{Semantic fault localization and suspiciousness ranking}}, doi = {10.1007/978-3-030-17462-0_13}, volume = {11427}, year = {2019}, } @inproceedings{6035, abstract = {We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.}, author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian}, booktitle = {Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control}, isbn = {9781450362825}, keywords = {reachability analysis, hybrid systems, lazy computation}, location = {Montreal, QC, Canada}, pages = {39--44}, publisher = {ACM}, title = {{JuliaReach: A toolbox for set-based reachability}}, doi = {10.1145/3302504.3311804}, volume = {22}, year = {2019}, } @inproceedings{6428, abstract = {Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.}, author = {Ferrere, Thomas and Nickovic, Dejan and Donzé, Alexandre and Ito, Hisahiro and Kapinski, James}, booktitle = {Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control}, isbn = {9781450362825}, location = {Montreal, Canada}, pages = {57--66}, publisher = {ACM}, title = {{Interface-aware signal temporal logic}}, doi = {10.1145/3302504.3311800}, year = {2019}, } @inproceedings{6462, abstract = {A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles.}, author = {Avni, Guy and Bloem, Roderick and Chatterjee, Krishnendu and Henzinger, Thomas A and Konighofer, Bettina and Pranger, Stefan}, booktitle = {31st International Conference on Computer-Aided Verification}, isbn = {9783030255398}, issn = {0302-9743}, location = {New York, NY, United States}, pages = {630--649}, publisher = {Springer}, title = {{Run-time optimization for learned controllers through quantitative games}}, doi = {10.1007/978-3-030-25540-4_36}, volume = {11561}, year = {2019}, } @inproceedings{6493, abstract = {We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.}, author = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian and Zeleznik, Luka}, booktitle = {31st International Conference on Computer-Aided Verification}, isbn = {9783030255398}, issn = {0302-9743}, keywords = {Synthesis, Linear hybrid automaton, Membership}, location = {New York City, NY, USA}, pages = {297--314}, publisher = {Springer}, title = {{Membership-based synthesis of linear hybrid automata}}, doi = {10.1007/978-3-030-25540-4_16}, volume = {11561}, year = {2019}, } @article{6752, abstract = {Two-player games on graphs are widely studied in formal methods, as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. The following bidding rule was previously defined and called Richman bidding. Both players have separate budgets, which sum up to 1. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a threshold budget in a vertex is a value t ∈ [0, 1] such that if Player 1’s budget exceeds t, he can win the game; and if Player 2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with random-turn games—a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players.}, author = {Avni, Guy and Henzinger, Thomas A and Chonev, Ventsislav K}, issn = {1557735X}, journal = {Journal of the ACM}, number = {4}, publisher = {ACM}, title = {{Infinite-duration bidding games}}, doi = {10.1145/3340295}, volume = {66}, year = {2019}, } @article{7109, abstract = {We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.}, author = {Ferrere, Thomas and Maler, Oded and Ničković, Dejan and Pnueli, Amir}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {3}, publisher = {ACM}, title = {{From real-time logic to timed automata}}, doi = {10.1145/3286976}, volume = {66}, year = {2019}, } @inproceedings{7147, abstract = {The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets. In this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest. The behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions.}, author = {Guet, Calin C and Henzinger, Thomas A and Igler, Claudia and Petrov, Tatjana and Sezgin, Ali}, booktitle = {17th International Conference on Computational Methods in Systems Biology}, isbn = {9783030313036}, issn = {1611-3349}, location = {Trieste, Italy}, pages = {155--187}, publisher = {Springer Nature}, title = {{Transient memory in gene regulation}}, doi = {10.1007/978-3-030-31304-3_9}, volume = {11773}, year = {2019}, } @inproceedings{7159, abstract = {Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. }, author = {Ničković, Dejan and Qin, Xin and Ferrere, Thomas and Mateis, Cristinel and Deshmukh, Jyotirmoy}, booktitle = {19th International Conference on Runtime Verification}, isbn = {9783030320782}, issn = {0302-9743}, location = {Porto, Portugal}, pages = {292--309}, publisher = {Springer Nature}, title = {{Shape expressions for specifying and extracting signal features}}, doi = {10.1007/978-3-030-32079-9_17}, volume = {11757}, year = {2019}, } @inproceedings{7231, abstract = {Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature.}, author = {Kong, Hui and Bartocci, Ezio and Jiang, Yu and Henzinger, Thomas A}, booktitle = {17th International Conference on Formal Modeling and Analysis of Timed Systems}, isbn = {978-3-0302-9661-2}, issn = {1611-3349}, location = {Amsterdam, The Netherlands}, pages = {123--141}, publisher = {Springer Nature}, title = {{Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty}}, doi = {10.1007/978-3-030-29662-9_8}, volume = {11750}, year = {2019}, }