-
A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
Authors:
Daisuke Ishii
Abstract:
The compositional approach is important for reasoning about large and complex systems. In this work, we address synchronous systems with hierarchical structures, which are often used to model cyber-physical systems. We revisit the theory of reactive modules and reformulate it based on hypergraphs to clarify the parallel composition and the hierarchical description of modules. Then, we propose an a…
▽ More
The compositional approach is important for reasoning about large and complex systems. In this work, we address synchronous systems with hierarchical structures, which are often used to model cyber-physical systems. We revisit the theory of reactive modules and reformulate it based on hypergraphs to clarify the parallel composition and the hierarchical description of modules. Then, we propose an automatic verification method for hierarchical systems. Given a system description annotated with assume-guarantee contracts, the proposed method divides the system into modules and verifies them separately to show that the top-level system satisfies its contract. Our method allows an input to be a circular system in which submodules mutually depend on each other. Experimental result shows our method can be effectively implemented using an SMT-based model checker.
△ Less
Submitted 16 March, 2024;
originally announced March 2024.
-
SMT-Based Model Checking of Industrial Simulink Models
Authors:
Daisuke Ishii,
Takashi Tomita,
Toshiaki Aoki,
The Quyen Ngo,
Thi Bich Ngoc Do,
Hideaki Takai
Abstract:
The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numericall…
▽ More
The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numerically accurate analysis of models, and (3) demonstrating the analysis of Simulink models using an SMT solver (we use Z3). It first encodes a target model into a predicate logic formula in the domain of mathematical arithmetic and bit vectors. We explore how to encode various Simulink blocks exactly. Then, the method verifies a given invariance property using the k-induction-based algorithm that extracts a subsystem involving the target block and unrolls the execution paths incrementally. In the experiment, we applied the proposed method and other tools to a set of models and properties. Our method successfully verified most of the properties including those unverified with other tools.
△ Less
Submitted 6 June, 2022;
originally announced June 2022.
-
Compositional Test Generation of Industrial Synchronous Systems
Authors:
Daisuke Ishii,
Takashi Tomita,
Kenji Onishi,
Toshiaki Aoki
Abstract:
Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexit…
▽ More
Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexity issue. We regard a test case as a counterexample in safety verification, and represent a test generation process as a deductive proof tree built with dedicated inference rules; we conduct both spatial- and temporal-compositional reasoning along with a modular system structure. A proof tree is generated using our semi-automated scheme involving manual effort on contract generation and automatic processes for counterexample search with SMT solvers. As case studies, the proposed method is applied to four industrial examples involving such features as enabled/triggered subsystems, multiple execution rates, filter components, and nested counters. In the experiments, we successfully generated test cases for target systems that were difficult to deal with using the existing tools.
△ Less
Submitted 10 December, 2021;
originally announced December 2021.
-
Approximate Translation from Floating-Point to Real-Interval Arithmetic
Authors:
Daisuke Ishii,
Takashi Tomita,
Toshiaki Aoki
Abstract:
Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes adv…
▽ More
Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes advantage of the efficiency of RA solving. The proposed method abstracts FP numbers as rational intervals and FPA expressions as interval arithmetic (IA) expressions; then, we solve IA formulas to check the satisfiability of an FPA formula using an off-the-shelf RA solver (we use CVC4 and Z3). In exchange for the efficiency gained by abstraction, the solving process becomes quasi-complete; we allow to output unknown when the satisfiability is affected by possible numerical errors. Furthermore, our IA is meticulously formalized to handle the special value NaN. We implemented the proposed method and compared it to four existing SMT solvers in the experiments. As a result, we confirmed that our solver was efficient for instances where rounding modes were parameterized.
△ Less
Submitted 6 December, 2021;
originally announced December 2021.
-
Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
Authors:
Daisuke Ishii,
Saito Fujii
Abstract:
One of the effective model checking methods is to utilize the efficient decision procedure of SAT (or SMT) solvers. In a SAT-based model checking, a system and its property are encoded into a set of logic formulas and the safety is checked based on the satisfiability of the formulas. As the encoding methods are improved and crafted (e.g., k-induction and IC3/PDR), verifying their correctness becom…
▽ More
One of the effective model checking methods is to utilize the efficient decision procedure of SAT (or SMT) solvers. In a SAT-based model checking, a system and its property are encoded into a set of logic formulas and the safety is checked based on the satisfiability of the formulas. As the encoding methods are improved and crafted (e.g., k-induction and IC3/PDR), verifying their correctness becomes more important. This research aims at a formal verification of the SMC methods using the Coq proof assistant. Our contributions are twofold: (1) We specify the basic encoding methods, k-induction and (a simplified version of) IC3/PDR in Coq as a set of simple and modular encoding predicates. (2) We provide a formal proof of the soundness of the encoding methods based on our formalized lemmas on state sequences and paths.
△ Less
Submitted 11 March, 2022; v1 submitted 24 June, 2020;
originally announced June 2020.
-
Computer-Assisted Verification of Four Interval Arithmetic Operators
Authors:
Daisuke Ishii,
Tomohito Yabu
Abstract:
Interval arithmetic libraries provide the four elementary arithmetic operators for operand intervals bounded by floating-point numbers. Actual implementations need to make a large case analysis that considers, e.g., magnitude relations between all pairs of argument bounds, positional relations between the arguments and zero, and handling of the special values, infinities and NaN. Their correctness…
▽ More
Interval arithmetic libraries provide the four elementary arithmetic operators for operand intervals bounded by floating-point numbers. Actual implementations need to make a large case analysis that considers, e.g., magnitude relations between all pairs of argument bounds, positional relations between the arguments and zero, and handling of the special values, infinities and NaN. Their correctness is not obvious as they are implemented by human hands, which comes to be critical for the reliability. This work provides a mechanically-verified interval arithmetic library. For this purpose, we utilize the Why3 platform equipped with a specification language for annotated programs and back-end theorem provers. We conduct several proof tasks for each of three properties of the target code: validity, soundness, and tightness; zero division exception handling is also verified for the division code. To accomplish the proof, we propose several techniques for specification/verification. First, we specify additional lemmas that support deductions made by back-end SMT solvers, which enable to discharge proof obligations in floating-point arithmetic containing nonlinear terms. Second, we examine the annotation of tightness, which requires to assume that a computation may result in NaN; we propose specific extremum operators for this purpose. In the experiments, applying the techniques in conjunction with the Alt-Ergo SMT solver and the Coq proof assistant proved the entire code.
△ Less
Submitted 8 April, 2020; v1 submitted 23 March, 2020;
originally announced March 2020.
-
Declarative Semantics of the Hybrid Constraint Language HydLa
Authors:
Kazunori Ueda,
Hiroshi Hosobe,
Daisuke Ishii
Abstract:
Hybrid systems are dynamical systems with continuous evolution of states and discrete evolution of states and governing equations. We have worked on the design and implementation of HydLa, a constraint-based modeling language for hybrid systems, with a view to the proper handling of uncertainties and the integration of simulation and verification. HydLa's constraint hierarchies facilitate the desc…
▽ More
Hybrid systems are dynamical systems with continuous evolution of states and discrete evolution of states and governing equations. We have worked on the design and implementation of HydLa, a constraint-based modeling language for hybrid systems, with a view to the proper handling of uncertainties and the integration of simulation and verification. HydLa's constraint hierarchies facilitate the description of constraints with adequate strength, but its semantical foundations are not obvious due to the interaction of various language constructs. This paper gives the declarative semantics of HydLa and discusses its properties and consequences by means of examples.
△ Less
Submitted 27 October, 2019;
originally announced October 2019.
-
HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on Interval Analysis
Authors:
Daisuke Ishii,
Alexandre Goldsztejn
Abstract:
We present HySIA: a reliable runtime verification tool for nonlinear hybrid automata (HA) and signal temporal logic (STL) properties. HySIA simulates an HA with interval analysis techniques so that a trajectory is enclosed sharply within a set of intervals. Then, HySIA computes whether the simulated trajectory satisfies a given STL property; the computation is performed again with interval analysi…
▽ More
We present HySIA: a reliable runtime verification tool for nonlinear hybrid automata (HA) and signal temporal logic (STL) properties. HySIA simulates an HA with interval analysis techniques so that a trajectory is enclosed sharply within a set of intervals. Then, HySIA computes whether the simulated trajectory satisfies a given STL property; the computation is performed again with interval analysis to achieve reliability. Simulation and verification using HySIA are demonstrated through several example HA and STL formulas.
△ Less
Submitted 2 December, 2017;
originally announced December 2017.
-
Monitoring Temporal Properties using Interval Analysis
Authors:
Daisuke Ishii,
Naoki Yonezaki,
Alexandre Goldsztejn
Abstract:
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by…
▽ More
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.
△ Less
Submitted 7 February, 2016;
originally announced February 2016.
-
Monitoring Bounded LTL Properties Using Interval Analysis
Authors:
Daisuke Ishii,
Naoki Yonezaki,
Alexandre Goldsztejn
Abstract:
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and ri…
▽ More
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and rigorous monitoring algorithm that demonstrates that the problem is decidable. This algorithm performs a forward simulation of a hybrid automaton, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. A continuous state at a certain time computed in each step is enclosed by an interval vector that is proven to contain a unique solution. In the experiments, we show that the proposed method provides a useful tool for formal analysis of nonlinear and complex hybrid systems.
△ Less
Submitted 14 July, 2015; v1 submitted 4 June, 2015;
originally announced June 2015.
-
Scalable Parallel Numerical Constraint Solver Using Global Load Balancing
Authors:
Daisuke Ishii,
Kazuki Yoshizoe,
Toyotaro Suzumura
Abstract:
We present a scalable parallel solver for numerical constraint satisfaction problems (NCSPs). Our parallelization scheme consists of homogeneous worker solvers, each of which runs on an available core and communicates with others via the global load balancing (GLB) method. The parallel solver is implemented with X10 that provides an implementation of GLB as a library. In experiments, several NCSPs…
▽ More
We present a scalable parallel solver for numerical constraint satisfaction problems (NCSPs). Our parallelization scheme consists of homogeneous worker solvers, each of which runs on an available core and communicates with others via the global load balancing (GLB) method. The parallel solver is implemented with X10 that provides an implementation of GLB as a library. In experiments, several NCSPs from the literature were solved and attained up to 516-fold speedup using 600 cores of the TSUBAME2.5 supercomputer.
△ Less
Submitted 18 May, 2015;
originally announced May 2015.
-
Scalable Parallel Numerical CSP Solver
Authors:
Daisuke Ishii,
Kazuki Yoshizoe,
Toyotaro Suzumura
Abstract:
We present a parallel solver for numerical constraint satisfaction problems (NCSPs) that can scale on a number of cores. Our proposed method runs worker solvers on the available cores and simultaneously the workers cooperate for the search space distribution and balancing. In the experiments, we attained up to 119-fold speedup using 256 cores of a parallel computer.
We present a parallel solver for numerical constraint satisfaction problems (NCSPs) that can scale on a number of cores. Our proposed method runs worker solvers on the available cores and simultaneously the workers cooperate for the search space distribution and balancing. In the experiments, we attained up to 119-fold speedup using 256 cores of a parallel computer.
△ Less
Submitted 6 November, 2014;
originally announced November 2014.
-
Strong correlation effects of the Re 5$d$ electrons on the metal-insulator transition in Ca$_2$FeReO$_6$
Authors:
H. Iwasawa,
T. Saitoh,
Y. Yamashita,
D. Ishii,
H. Kato,
N. Hamada,
Y. Tokura,
D. D. Sarma
Abstract:
We have investigated the electronic structure of polycrystalline Ca$_2$FeReO$_6$ using photoemission spectroscopy and band-structure calculations within the local-density approximation+$U$ (LDA+$U$) scheme. In valence-band photoemission spectra, a double-peak structure which is characteristic of the metallic double perovskite series has been observed near the Fermi level ($E_{\rm F}$), although…
▽ More
We have investigated the electronic structure of polycrystalline Ca$_2$FeReO$_6$ using photoemission spectroscopy and band-structure calculations within the local-density approximation+$U$ (LDA+$U$) scheme. In valence-band photoemission spectra, a double-peak structure which is characteristic of the metallic double perovskite series has been observed near the Fermi level ($E_{\rm F}$), although it is less distinct compared to the Sr$_2$FeMoO$_6$ case. The leading near-$E_{\rm F}$ structure has a very weak spectral weight at $E_{\rm F}$ above the metal-insulator transition (MIT) temperature $T_{\rm MI}$ of $\sim$140 K, and it loses the $E_{\rm F}$ weight below $T_{\rm MI}$, forming a small energy gap.
To reproduce this small energy gap in the calculation, we require a very large effective $U$ ($U_{\rm eff}$) for Re (4 eV) in addition to a relatively large $U_{\rm eff}$ for Fe (4 eV). Although the most of the experimental features can be interpreted with the help of the band theory, the overall agreement between the theory and the experiment was not satisfactory. We demonstrate that the effective transfer integral between Fe and Re is actually smaller than that between Fe and Mo in Ca$_2$FeMoO$_6$, which can explain both MIT and very high ferrimagnetic transition temperature.
△ Less
Submitted 29 November, 2004;
originally announced November 2004.
