JumpSAT Based System Verification Scenarios

Author(s):  
Andrzej Pulka
Keyword(s):  
2014 ◽  
Vol 668-669 ◽  
pp. 879-883 ◽  
Author(s):  
Yi Gang Sun ◽  
Li Sun

In order to avoid the complex mathematical modeling and ensure the reliability of avionics system verification, this paper has designed an interfaces emulation and verification platform of avionics system based on QAR data. Platform includes 2 parts: Emulator and Simulator. Simulator generates the flight environmental data which is come from QAR and transforms the data into excitation signal of devices. Emulator emulates the interface features of avionic devices according to the ICD and can be replaced with real devices. By comparing the actual input-output data of devices with QAR theoretical data, this platform can evaluate the running performance of avionic systems or devices and the rationality of the ICD.


2003 ◽  
Vol 68 (5) ◽  
pp. 85-100 ◽  
Author(s):  
C. Bui Thanh ◽  
H. Klaudel ◽  
F. Pommereau

Author(s):  
Zhe Dong ◽  
Yifei Pan ◽  
Miao Liu ◽  
Xiaojin Huang

The nuclear heating reactor (NHR) is a typical integral pressurized water reactor (iPWR) developed by the institute of nuclear and new energy technology (INET) of Tsinghua University, which has the safety advanced features such as the primary circuit integral arrangement, full-range natural circulation, self-pressurization. Power-level control is crucial for the operational stability and efficiency of the NHR, and the dynamic modeling is a basis for control system design and verification. From the conservation laws of mass, energy and momentum, a lumped-parameter dynamical model is proposed for the nuclear steam supply system (NSSS) based on the 200MWth nuclear heating reactor II (NHR200-II). The steady-state model validation is given by the comparing the parameter values of this model and that for plant design. Then, both the open-loop responses under the disturbances of reactivity and coolant flowrates as well as the closed-loop responses under the case of power ramp are given, where the rationality of the responses are analyzed from the viewpoint of plant physics and thermal-hydraulics. This model can be utilized for not only the control system design but also the development of a real-time simulator for the hardware-in-loop control system verification.


10.29007/59rn ◽  
2018 ◽  
Author(s):  
Amit Goel ◽  
Sava Krstic ◽  
Rebekah Leslie ◽  
Mark Tuttle

We introduce the <i>Deductive Verificaton Framework</i> (DVF), a language and a tool for verifying properties of transition systems. The language is procedural and the system transitions are a selected subset of procedures. The type system and built-in operations are consistent with SMT-LIB, as are the multisorted first-order logical formulas that may occur in DVF programs as pre- and post-conditions, assumptions, assertions, and goals. A template mechanism allows parametric specification of complex types within the confines of this logic. Verification conditions are generated from specified goals and passed to SMT engine(s). A general assume-guarantee scheme supports a thin layer of interactive proving.


10.29007/1kq2 ◽  
2018 ◽  
Author(s):  
Chuchu Fan ◽  
Parasara Sridhar Duggirala ◽  
Sayan Mitra ◽  
Mahesh Viswanathan

In this paper, we present the progress we have made in verifying the benchmark powertrain control systems introduced in the last ARCH workshop. We implemented the algorithm for computing local discrepancy (rate of convergence or divergence of trajectories) reported in the hybrid system verification tool C2E2. We created Stateflow translations of the original models to aid the processing using C2E2 tool. We also had to encode the different driver behaviors in the form of state machines. With these customizations, we have been successful in verifying one of the easier (but still challenging) benchmarks from the powertrain suite. In this paper, we present some of the engineering challenges and describe the artifacts we created in the process.


Sign in / Sign up

Export Citation Format

Share Document