@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}, } @inproceedings{142, abstract = {We address the problem of analyzing the reachable set of a polynomial nonlinear continuous system by over-approximating the flowpipe of its dynamics. The common approach to tackle this problem is to perform a numerical integration over a given time horizon based on Taylor expansion and interval arithmetic. However, this method results to be very conservative when there is a large difference in speed between trajectories as time progresses. In this paper, we propose to use combinations of barrier functions, which we call piecewise barrier tube (PBT), to over-approximate flowpipe. The basic idea of PBT is that for each segment of a flowpipe, a coarse box which is big enough to contain the segment is constructed using sampled simulation and then in the box we compute by linear programming a set of barrier functions (called barrier tube or BT for short) which work together to form a tube surrounding the flowpipe. The benefit of using PBT is that (1) BT is independent of time and hence can avoid being stretched and deformed by time; and (2) a small number of BTs can form a tight over-approximation for the flowpipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype called PBTS in C++. Experiments on some benchmark systems show that our approach is effective.}, author = {Kong, Hui and Bartocci, Ezio and Henzinger, Thomas A}, location = {Oxford, United Kingdom}, pages = {449 -- 467}, publisher = {Springer}, title = {{Reachable set over-approximation for nonlinear systems using piecewise barrier tubes}}, doi = {10.1007/978-3-319-96145-3_24}, volume = {10981}, year = {2018}, } @article{434, abstract = {In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.}, author = {Jiang, Yu and Liu, Han and Song, Huobing and Kong, Hui and Wang, Rui and Guan, Yong and Sha, Lui}, journal = {IEEE Transactions on Intelligent Transportation Systems}, number = {10}, pages = {3320 -- 3333}, publisher = {IEEE}, title = {{Safety-assured model-driven design of the multifunction vehicle bus controller}}, doi = {10.1109/TITS.2017.2778077}, volume = {19}, year = {2018}, } @inproceedings{663, abstract = {In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u→, x→) = 0, parametric in u→, which can yield an infinite number of concrete invariants by assigning different values to u→ so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial right-hand sides, given a template multivariate polynomial g(u→, x→), an invariant cluster can be obtained by first computing the remainder of the Lie derivative of g(u→, x→) divided by g(u→, x→) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is efficient. }, author = {Kong, Hui and Bogomolov, Sergiy and Schilling, Christian and Jiang, Yu and Henzinger, Thomas A}, booktitle = {Proceedings of the 20th International Conference on Hybrid Systems}, isbn = {978-145034590-3}, location = {Pittsburgh, PA, United States}, pages = {163 -- 172}, publisher = {ACM}, title = {{Safety verification of nonlinear hybrid systems based on invariant clusters}}, doi = {10.1145/3049797.3049814}, year = {2017}, } @inproceedings{647, abstract = {Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems.}, author = {Bogomolov, Sergiy and Giacobbe, Mirco and Henzinger, Thomas A and Kong, Hui}, isbn = {978-331965764-6}, location = {Berlin, Germany}, pages = {116 -- 132}, publisher = {Springer}, title = {{Conic abstractions for hybrid systems}}, doi = {10.1007/978-3-319-65765-3_7}, volume = {10419 }, year = {2017}, } @inproceedings{1227, abstract = {Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.}, author = {Kong, Hui and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Henzinger, Thomas A and Jiang, Yu and Schilling, Christian}, location = {Grenoble, France}, pages = {128 -- 144}, publisher = {Springer}, title = {{Discrete abstraction of multiaffine systems}}, doi = {10.1007/978-3-319-47151-8_9}, volume = {9957}, year = {2016}, } @inproceedings{1256, abstract = {Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform.}, author = {Jiang, Yu and Yang, Yixiao and Liu, Han and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui}, location = {Vienna, Austria}, publisher = {IEEE}, title = {{From stateflow simulation to verified implementation: A verification approach and a real-time train controller design}}, doi = {10.1109/RTAS.2016.7461337}, year = {2016}, } @inproceedings{479, abstract = {Clinical guidelines and decision support systems (DSS) play an important role in daily practices of medicine. Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care. During the collaboration with Carle hospital to develop a DSS, we identify that, for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties in guidelines, which brings new challenges to current simulation based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios, and applied the proposed technique to assist existing DSS. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital}, author = {Jiang, Yu and Liu, Han and Kong, Hui and Wang, Rui and Hosseini, Mohamad and Sun, Jiaguang and Sha, Lui}, booktitle = {Proceedings of the 38th International Conference on Software Engineering Companion }, location = {Austin, TX, USA}, pages = {112 -- 121}, publisher = {IEEE}, title = {{Use runtime verification to improve the quality of medical care practice}}, doi = {10.1145/2889160.2889233}, year = {2016}, } @inproceedings{1205, abstract = {In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.}, author = {Jiang, Yu and Liu, Han and Song, Houbing and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui}, location = {Limassol, Cyprus}, pages = {757 -- 763}, publisher = {Springer}, title = {{Safety assured formal model driven design of the multifunction vehicle bus controller}}, doi = {10.1007/978-3-319-48989-6_47}, volume = {9995}, year = {2016}, } @inproceedings{1605, abstract = {Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.}, author = {Bogomolov, Sergiy and Schilling, Christian and Bartocci, Ezio and Batt, Grégory and Kong, Hui and Grosu, Radu}, location = {Haifa, Israel}, pages = {19 -- 35}, publisher = {Springer}, title = {{Abstraction-based parameter synthesis for multiaffine systems}}, doi = {10.1007/978-3-319-26287-1_2}, volume = {9434}, year = {2015}, }