Using Model Checking to Verify the Logic Module of Flight Control Software

Shun Kun Yang; Guo Qi Li

doi:10.4028/www.scientific.net/AMM.341-342.655

Paper Titles

Cigarette Filter Rod Parameter Measure Based on Otsu Image Processing
p.635

Design and Application of a Flamethrower Robot in Getting Rid of Foreign Matter on Power Transmission Lines
p.640

Home Services - Track Transport Robot Control System Design
p.646

Design of Toxic Gas Monitoring System Based on Virtual Technology and WSN
p.650

Using Model Checking to Verify the Logic Module of Flight Control Software
p.655

The Design of Temperature Control System for Rice Wine Fermentation
p.660

Study of Fuzzy-PID Control in MATLAB for Two-Phase Hybrid Stepping Motor
p.664

Fuzzy Control for Nonlinear Uncertain T-S Fuzzy Systems with Time-Varying Delays
p.668

Design of Vehicle Navigation Terminal Interface Based on QT
p.674

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 341-342Using Model Checking to Verify the Logic Module of...

Using Model Checking to Verify the Logic Module of Flight Control Software

Abstract:

Model checking is an important method to verify state machine based system. In this paper, we using PAT, a novel and powerful model checking tool, to verify the logic module of flight control software, which is public available. Conclusions are drawn from the verification and these are valuable for similar researches.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 341-342)

Pages:

655-659

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.341-342.655

Citation:

Cite this paper

Online since:

July 2013

Authors:

Shun Kun Yang, Guo Qi Li

Keywords:

Flight Control, Logic Module, Model Checking

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] P. Doron, P. Patrizio and S. Paola. Model Checking, Wiley Encyclopedia of Computer Science and Engineering, (2009).

Google Scholar

[2] H. Constance, K.J. James, L. Bruce, A. Myla and B. Ramesh, Using abstraction and model checking to detect safety violations in requirements specifications. J. IEEE transaction on software engineering. 24(1998)927-948.

DOI: 10.1109/32.730543

Google Scholar

[3] C. Lucas, F. Bernd and M. Joao, SMT-based bounded model checking for embedded ANSI-C software. J. IEEE transaction on software engineering. 38(2012)957-974.

DOI: 10.1109/tse.2011.59

Google Scholar

[4] C. William, A.J. Richard, B. Paul, J.H. David, N. David and W.E. William, Optimizing symbolic model checking for statecharts. J. IEEE transaction on software engineering. 27(2001)170-190.

Google Scholar

[5] PAT: Process Analysis Toolkit An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems, available at http: /www. comp. nus. edu. sg/~pat.

Google Scholar