Article

Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report

Authors:

Murali Rangarajan,

Bruno DutertreAuthors Info & Claims

ICSE '04: Proceedings of the 26th International Conference on Software Engineering

Pages 304 - 313

Published: 23 May 2004 Publication History

Abstract

The hardware and software in modern aircraft control systems are good candidates for verification using formal methods: they are complex, safety-critical, and challenge the capabilities of test-based verification strategies. We have previously reported on our use of model checking to verify the time partitioning property of the Deos real-time operating system for embedded avionics. The size and complexity of this system have limited us to analyzing only one configuration at a time. To overcome this limit and generalize our analysis to arbitrary configurations we have turned to theorem proving.This paper describes our use of the PVS theorem prover to analyze the Deos scheduler. In addition to our inductive proof of the time partitioning invariant, we present a feature-based technique for modeling state-transition systems and formulating inductive invariants. This technique facilitates an incremental approach to theorem proving that scales well to models of increasing complexity, and has the potential to be applicable to a wide range of problems.

References

[1]

{1} K. Altisen, G. Gößler, and J. Sifakis. A Methodology for the Construction of Scheduled Systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Pune, India, September 2000. To appear.

[2]

{2} P. Binns. A robust high-performance time partitioning algorithm: the digital engine operating system (deos) approach. In Proceedings of the 20th Digital Avionics System Conference , 2001.

[3]

{3} S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing Quantitative Characteristics of Finite-State Real-Time Systems. In IEEE Real-Time Systems Symposium , pages 266-270, 1994.

[4]

{4} D. Cofer and M. Rangarajan. Formal modeling and analysis of advanced scheduling features in an avionics rtos. In 2nd International Conferenceon Embedded Software, EMSOFT, 2002.

Digital Library

[5]

{5} D. Cofer and M. Rangarajan. Formal verification of overhead accounting in an avionics rtos. In IEEE Real Time Systems Symposium, 2002.

Digital Library

[6]

{6} B. Dutertre. Formal Analysis of the Priority Ceiling Protocol. In IEEE Real-Time Systems Symposium (RTSS'00), pages 151-160, Orlando, FL, November 2000.

Digital Library

[7]

{7} B. Dutertre, H. Saïdi, and V. Stavridou. Intrusion-Tolerant Group Management in Enclaves. In International Conference on Dependable Systems and Networks (DSN'01), pages 203-212, Göteborg, Sweden, July 2001.

Digital Library

[8]

{8} S. Fowler and A. Wellings. Formal Development of a Real-Time Kernel. In Proceedings of the IEEE Real-Time Systems Symposium, pages 220-229, December 1997.

Digital Library

[9]

{9} G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997.

Digital Library

[10]

{10} J. P. Lehoczky and S. Ramos-Thuel. An optimal algorithm for scheduling aperiodic tasks in fixed-priority preemptive systems. In Proceedings of the IEEE Real-Time Systems Symposium, December 1992.

[11]

{11} C. Liu and J. Layland. Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. Journal of the ACM, 20(1):46-61, January 1973.

Digital Library

[12]

{12} Z. Manna and A. Pnueli. Temporal Verification Diagrams. In International Symposium on Theoretical Aspects of Computer Software (TACS'94), volume 789 of Lecture Notes in Computer Science, pages 726-765, Sendai, Japan, April 1994. Springer-Verlag.

Digital Library

[13]

{13} J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger. Verification of time partitioning in the DEOS scheduler kernel. In International Conference on Software Engineering, pages 488-497, 2000.

Digital Library

[14]

{14} H. Pfeifer. Formal Verification of the TTP Group Membership Algorithm. In FORTE/PSTV 2000, Pisa, Italy, October 2000.

Digital Library

[15]

{15} RTCA. Software Considerations in Airborne Systems and Equipment Certification, DO-178B, 1992.

[16]

{16} J. Rushby. Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. In Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes in Computer Science, pages 508-520, Chicago, IL, July 2000. Springer-Verlag.

Digital Library

[17]

{17} S. Vestal. Formal Verification of the MetaH Executive Using Linear Hybrid Automata. In Proceedings of the 6th IEEE Real-Time Technology and Application Symposium (RTAS'2000), pages 134-144, Washington, DC, May-June 2000.

Digital Library

[18]

{18} M. Wilding. A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. In Computer-Aided Verification - CAV'98, volume 1427 of Lecture Notes in Computer Science, pages 369-378, Vancouver, Canada, June-July 1998. Springer-Verlag.

Digital Library

[19]

{19} Z. Yuhua and Z. Chaochen. A Formal Proof of the Deadline Driven Scheduler. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 756-775, Lubeck, Germany, September 1994. Springer Verlag.

Digital Library

Cited By

Zhao YSanan DZhang FLiu Y(2019)Refinement-Based Specification and Security Analysis of Separation KernelsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2017.267298316:1(127-141)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1109/TDSC.2017.2672983
Zhao YYang ZMa D(2017)A survey on formal specification and verification of separation kernelsFrontiers of Computer Science: Selected Publications from Chinese Universities10.5555/3128671.312868111:4(585-607)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.5555/3128671.3128681
Åsberg MNolte T(2013)Towards a user-mode approach to partitioned scheduling in the seL4 microkernelACM SIGBED Review10.1145/2544350.254435210:3(15-22)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1145/2544350.2544352
Show More Cited By

Index Terms

Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
      2. Formal methods
        Model checking
    2. Software system structures
      1. Software system models
        State systems
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

SAT-based Abstraction Refinement for Real-time Systems

In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic ...
Programming inductive proofs: a new approach based on contextual types
Verification, induction termination analysis

In this paper, we present an overview to programming with proofs in the reasoning framework, Beluga. Beluga supports the specification of formal systems given by axioms and inference rules within the logical framework LF. It also supports implementing ...
Programming inductive proofs: a new approach based on contextual types
Verification, induction termination analysis

In this paper, we present an overview to programming with proofs in the reasoning framework, Beluga. Beluga supports the specification of formal systems given by axioms and inference rules within the logical framework LF. It also supports implementing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '04: Proceedings of the 26th International Conference on Software Engineering

May 2004

761 pages

ISBN:0769521630

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

IEEE Computer Society

United States

Publication History

Published: 23 May 2004

Check for updates

Qualifiers

Article

Conference

ICSE04

Sponsor:

SIGSOFT

ICSE04: 26th International Conference on Software Engineering

May 23 - 28, 2004

Acceptance Rates

ICSE '04 Paper Acceptance Rate 58 of 436 submissions, 13%;

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
357
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhao YSanan DZhang FLiu Y(2019)Refinement-Based Specification and Security Analysis of Separation KernelsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2017.267298316:1(127-141)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1109/TDSC.2017.2672983
Zhao YYang ZMa D(2017)A survey on formal specification and verification of separation kernelsFrontiers of Computer Science: Selected Publications from Chinese Universities10.5555/3128671.312868111:4(585-607)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.5555/3128671.3128681
Åsberg MNolte T(2013)Towards a user-mode approach to partitioned scheduling in the seL4 microkernelACM SIGBED Review10.1145/2544350.254435210:3(15-22)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1145/2544350.2544352
Rangarajan MCofer D(2007)Computing worst-case response times in real-time avionics applicationsProceedings of the 12th international conference on Formal methods for industrial critical systems10.5555/1793603.1793614(101-114)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.5555/1793603.1793614

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents