Verification of time partitioning in the DEOS scheduler kernel

ABSTRACT

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. To conduct the experiment, a core slice of the DEOS scheduling kernel was first translated without abstraction from C++ into Promela (the input language for Spin). We constructed an abstract “test-driver” environment and carefully introduced several abstractions into the system to support verification. Several experiments were run to attempt to verify that the system implementation adhered to the critical time partitioning requirements. During these experiments, the known error was rediscovered in the time partitioning implementation. We believe this case study provides several insights into how to develop cost-effective methods and tools to support the software design and implementation review process.

REFERENCES

• 1: Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.156-166, October 16-18, 1996, San Francisco, California, United States
• 2: Pam Binns. Design document for slack scheduling in deos, draft alpha.3. Honeywell, September 1998.
• 3: William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302460]
• 4: Edmund M. Clarke , Orna Grumberg , David E. Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.124-175, June 01-04, 1993
• 5: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: Zhe Dang , Richard A. Kemmerer, Using the ASTRAL model checker to analyze mobile IP, Proceedings of the 21st international conference on Software engineering, p.132-141, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302459]
• 8: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 9: Claudio Demartini , Radu Iosif , Riccardo Sisto, dSPIN: A Dynamic Extension of SPIN, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.261-276, September 21-24, 1999
• 10: Matthew B. Dwyer , Corina S. Pasareanu, Filter-based model checking of partial systems, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.189-202, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 11: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 12: John Hatcliff , Matthew B. Dwyer , Shawn Laubach, Staging Static Analyses Using Abstraction-Based Program Specialization, Proceedings of the 10th International Symposium on Principles of Declarative Programming, p.134-151, September 16-18, 1998
• 13: K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 1999.
• 14: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 15: Gerard J. Holzmann , Margaret H. Smith, Software Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.481-497, October 05-08, 1999
• 16: J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger. Translation and verification of the DEOS scheduling kernel. Technical report, NASA Ames Research Center / Honeywell Technology Center, October 1999.
• 17: Corina S. Pasareanu , Matthew B. Dwyer , Michael Huth, Assume-Guarantee Model Checking of Software: A Comparative Case Study, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.168-183, September 21-24, 1999
• 18: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 19: RTCA Special Committee 167. Software considerations in airborne systems and equipment certification. Technical Report DO-178B, RTCA, Inc., dec 1992.
• 20: Tomas E. Uribe Restrepo , Zohar Manna, Abstraction-based deductive-algorithmic verification of reactive systems, 1999
• 21: W. Visser, K. Havelund, and J. Penix. Adding Active Objects to SPIN. In Proceedings of the 5th SPIN Workshop, Trento, Italy, July 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Threads

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Sequencing and scheduling

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Scheduling

General Terms:
Design, Experimentation, Performance, Reliability, Theory, Verification