@ARTICLE{ iet:/content/journals/10.1049/iet-cps.2016.0042, author = {Hao Ren}, affiliation = { Department of Electrical and Computer Engineering, Iowa State University, Ames, IA 50014, USA }, author = {Jing Huang}, affiliation = { Technology and Operations, NXP Semiconductors, Austin, TX 78735, USA }, author = {Shengbing Jiang}, affiliation = { Vehicle Health Management Group, General Motors, Warren, MI 48090, USA }, author = {Ratnesh Kumar}, affiliation = { Department of Electrical and Computer Engineering, Iowa State University, Ames, IA 50014, USA }, keywords = {safety verification;discrete state reachability;Fischer mutual exclusion protocol;symbolic verifier;LHA;satisfiability modulo theory solver;purely discrete linear transition system;counterexample fragment based specification relaxation;concurrent linear hybrid automaton;CEFSR framework;LhaVrf;unsatisfiable core;modular linear hybrid automata;}, language = {English}, abstract = {We present LhaVrf, a symbolic verifier for the safety verification of concurrent LHA (Linear Hybrid Automaton). A concurrent LHA is composed of a set of LHAs that interact through shared variables and/or events. An LHA is first translated to a purely discrete linear transition system that preserves the reachability of discrete states. Its analysis can be conducted in the proposed counterexample fragment based specification relaxation (CEFSR) framework, where an invalid fragment of a counterexample is used to eliminate the entire set of counterexamples sharing the same fragment, by way of specification relaxation (as opposed to the traditional model refinement). For concurrent systems, we propose further enhancement towards scalability as follows. For each spurious counterexample, an unsatisfiable core (unsat-core) that makes the counterexample invalid, is identified and used for specification relaxation, thereby eliminating the entire set of spurious counterexamples sharing the same unsat-core in a single iteration. Our implementation of LhaVrf adopts the above key ideas, with capability of automatically translating the hybrid automata into discrete transition system, composing the concurrent model, and using satisfiability modulo theory solver for validating counterexamples and fast-searching for the unsat-core. The verifier is illustrated via an application to the Fischer mutual exclusion protocol.}, title = {Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata}, journal = {IET Cyber-Physical Systems: Theory & Applications}, issue = {2}, volume = {2}, year = {2017}, month = {July}, pages = {65-74(9)}, publisher ={Institution of Engineering and Technology}, copyright = {This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)}, url = {https://digital-library.theiet.org/;jsessionid=26q97k7ke1utb.x-iet-live-01content/journals/10.1049/iet-cps.2016.0042} }