Application of design for verification with concurrency controllers to air traffic control software

ABSTRACT

We present an experimental study which demonstrates that model checking techniques can be effective in finding synchronization errors in safety critical software when they are combined with a design for verification approach. We apply the concurrency controller design pattern to the implementation of the synchronization operations in Java programs. This pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them using interfaces specified as finite state machines. The behavior of a concurrency controller can be verified with respect to arbitrary numbers of threads using infinite state model checking techniques, and the threads which use the controller classes can be checked for interface violations using finite state model checking techniques. We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted an experimental study investigating the effectiveness of the presented design for verification approach on safety critical air traffic control software. In this study, we first reengineered the Tactical Separation Assisted Flight Environment (TSAFE) software using the concurrency controller design pattern. Then, using fault seeding, we created 40 faulty versions of TSAFE and used both infinite and finite state verification techniques for finding the seeded faults. The experimental study demonstrated the effectiveness of the presented modular verification approach and resulted in a classification of faults that can be found using the presented approach.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 2: Aysu Betin-Can , Tevfik Bultan, Verifiable Concurrent Programming Using Concurrency Controllers, Proceedings of the 19th IEEE international conference on Automated software engineering, p.248-257, September 20-24, 2004 [doi>10.1109/ASE.2004.75]
• 3: Aysu Betin-Can , Tevfik Bultan , Xiang Fu, Design for verification for asynchronously communicating Web services, Proceedings of the 14th international conference on World Wide Web, May 10-14, 2005, Chiba, Japan [doi>10.1145/1060745.1060853]
• 4: Jeffrey George Bogda , Ambuj Singh , Urs Holzle, Program analysis alleviates java synchronization, 2001
• 5: Tevfik Bultan , Tuba Yavuz-Kahveci, Action Language Verifier, Proceedings of the 16th IEEE international conference on Automated software engineering, p.382, November 26-29, 2001
• 6: T. Cargill. Specific notification for Java thread synchronization. In Proc. of the 3rd PLoP, 1996.
• 7: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 8: Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , Marcin Jurdzinski , Freddy Y. C. Mang, Interface Compatibility Checking for Software Modules, Proceedings of the 14th International Conference on Computer Aided Verification, p.428-441, July 27-31, 2002
• 9: R. DeLine and M. Fahndrich. Typestates for objects. In Proc. of ECOOP, pages 465--490, 2004.
• 10: G. Dennis. TSAFE: Building a trusted computing base for air traffic control software, Master's Thesis, 2003.
• 11: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 12: Matthew B. Dwyer , Robby , Oksana Tkachuk , Willem Visser, Analyzing Interaction Orderings with Model Checking, Proceedings of the 19th IEEE international conference on Automated software engineering, p.154-163, September 20-24, 2004 [doi>10.1109/ASE.2004.11]
• 13: H. Erzberger. The automated airspace concept. In Proc. of USA/Europe Air Traffic Management R&D Seminar, 2001.
• 14: H. Erzberger. Transforming the NAS: The next generation air traffic control system. In Proc. of the 24th Int. Congress of the Aeronautical Sciences, 2004.
• 15: Advance automation system. Dep. of Transportation, Office of Inspector General, Audit Report, AV-1998-113, 1998.
• 16: C. Flanagan and S. Qadeer. Thread-modular model checking. In Proc. of the SPIN Workshop, pages 213--224, 2003.
• 17: Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.345-357, June 17-19, 1998, Montreal, Quebec, Canada
• 18: Indus. http://indus.projects.cis.ksu.edu.
• 19: Doug Lea , Douglas Lea, Concurrent Programming in Java. Second Edition: Design Principles and Patterns, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 20: M. Lindvall and et al. An evolutionary testbed for software technology evaluation. NASA Journal of Innovations in Systems and Software Engineering, 1(1):3-11, 2005.
• 21: P. C. Mehlitz and J. Penix. Design for verification using design patterns to build reliable systems. In Workshop on Component-Based Soft. Eng., 2003.
• 22: Karl J. Ottenstein , Linda M. Ottenstein, The program dependence graph in a software development environment, Proceedings of the first ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.177-184, April 1984
• 23: Natasha Sharygina , James C. Browne , Robert P. Kurshan, A Formal Object-Oriented Analysis for Software Reliability: Design for Verification, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.318-332, April 02-06, 2001
• 24: Soot: a java optimization framework. http://www.sable.mcgill.ca/soot/.
• 25: Scott D. Stoller , Yanhong A. Liu, Transformations for model checking distributed Java programs, Proceedings of the 8th international SPIN workshop on Model checking of software, p.192-199, May 2001, Toronto, Ontario, Canada
• 26: O. Tkachuk and M. B. Dwyer. Adapting side-effects analysis for modular program model checking. In Proc. of ASE, pages 188--197, 2003.
• 27: O. Tkachuk, M. B. Dwyer, and C. Pasareanu. Automated environment generation for software model checking. In Proc. of ESEC/FSE, pages 116--129, 2003.
• 28: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 29: Tuba Yavuz-Kahveci , Tevfik Bultan, Specification, verification, and synthesis of concurrency control components, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking

General Terms:
Design, Verification

Keywords:
concurrent programming, design patterns, interfaces, model checking, synchronization