Scenario-based timing verification of multiprocessor embedded applications

ABSTRACT

This work presents a static timing-analysis method for verification of scenario-based real-time properties, on graphical task-level models of embedded applications. Scenario-based properties specify timing constraints which must be honored for specific control-flow behaviors and task execution orderings. Static checking of scenario-based properties currently requires computationally expensive model checking methods. Hence the proposed graph-based static timing-analysis algorithm improves upon the state-of-the-art. This is manifested in a significant performance advantage over timed model checking (up to 1000X in several cases), which suffers from state space explosion. The proposed algorithm also employs compositional reasoning and abstraction refinement for handling large problems. We also illustrate methods for using scenario-based timing analysis, which can act as alternatives to traditional timed model checking for verification of timed systems like FDDI and Fischer protocols. We implement this timing verification algorithm as a tool called SymTime and present experimental results for SymTime comparing it with SPIN, UPPAAL, and a TCTL model checker for Time Petri Nets, called Romeo.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, An old-fashioned recipe for real time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1543-1571, Sept. 1994 [doi>10.1145/186025.186058]
• 2: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 3: James F. Allen, Maintaining knowledge about temporal intervals, Communications of the ACM, v.26 n.11, p.832-843, Nov. 1983 [doi>10.1145/182.358434]
• 4: Alur, R., Courcoubetis, C., and Dill, D. L. 1990. Model-Checking for real-time systems. In Annual IEEE Symposium on Logic in Computer Science (LICS'90). IEEE Computer Society, 414--425.
• 5: Alur, R. and Dill, D. 1996. Automata-theoretic verification of real-time systems. In Formal Methods for Real-Time Computing. Trends in Sofware Series, John Wiley and Sons, 55--82.
• 6: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 7: Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994 [doi>10.1145/174644.174651]
• 8: R. Iris Bahar , Erica A. Frohm , Charles M. Gaona , Gary D. Hachtel , Enrico Macii , Abelardo Pardo , Fabio Somenzi, Algebraic decision diagrams and their applications, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.188-191, November 07-11, 1993, Santa Clara, California, United States
• 9: Bahar, R. I., Hachtel, G. D., Macii, E., Pardo, A., Poncino, M., and Somenzi, F. 1994. An ADD-based algorithm for shortest path back-tracing of large graphs. In VLSI Great Lakes Symposium, 248--251.
• 10: P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000 [doi>10.1145/349194.349197]
• 11: Beyer, D., Lewerentz, C., and Noack, A. 2003. Rabbit: A tool for BDD-based verification of real-time systems. In International Conference on Computer-Aided Verification (CAV), W. A. H. Jr. and F. Somenzi, Eds. Lecture Notes in Computer Science, vol. 2725. Springer, 122--125.
• 12: Victor Braberman , Nicolas Kicillof , Alfredo Olivero, A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties, IEEE Transactions on Software Engineering, v.31 n.12, p.1028-1041, December 2005 [doi>10.1109/TSE.2005.131]
• 13: Supratik Chakraborty , David L. Dill, Approximate algorithms for time separation of events, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.190-194, November 09-13, 1997, San Jose, California, United States
• 14: Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003 [doi>10.1145/876638.876643]
• 15: Clarke, E. M., Grumberg, O., and Peled, D., Eds. 2001. Model Checking. The MIT Press.
• 16: Patrick Cousot, Abstract interpretation, ACM Computing Surveys (CSUR), v.28 n.2, p.324-328, June 1996 [doi>10.1145/234528.234740]
• 17: Dipankar Das , P. P. Chakrabarti , Rajeev Kumar, Functional verification of task partitioning for multiprocessor embedded systems, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.4, p.44-es, September 2007 [doi>10.1145/1278349.1278357]
• 18: Ali Dasdan , Dinesh Ramanathan , Rajesh K. Gupta, A timing-driven design and validation methodology for embedded real-time systems, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.4, p.533-553, Oct. 1998 [doi>10.1145/296333.296338]
• 19: C. Daws , A. Olivero , S. Tripakis , S. Yovine, The tool KRONOS, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.208-219, July 1996, New Brunswick, NeW Jersey, United States
• 20: C. Daws , A. Olivero , S. Tripakis , S. Yovine, The tool KRONOS, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.208-219, July 1996, New Brunswick, NeW Jersey, United States
• 21: David L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.197-212, June 12-14, 1989
• 22: Rik Eshuis, Symbolic model checking of UML activity diagrams, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.1, p.1-38, January 2006 [doi>10.1145/1125808.1125809]
• 23: Gardey, G., Lime, D., Magnin, M., and Roux, O. H. 2005. Romeo: A tool for analyzing time petri nets. In International Conference on Computer-Aided Verification (CAV), K. Etessami and S. K. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer, 418--423.
• 24: M. R. Guthaus , J. S. Ringenberg , D. Ernst , T. M. Austin , T. Mudge , R. B. Brown, MiBench: A free, commercially representative embedded benchmark suite, Proceedings of the Workload Characterization, 2001. WWC-4. 2001 IEEE International Workshop, p.3-14, December 02-02, 2001 [doi>10.1109/WWC.2001.15]
• 25: Hendriks, M., Behrmann, G., Larsen, K. G., Niebert, P., and Vaandrager, F. W. 2003. Adding symmetry reduction to Uppaal. See Larsen and Niebert {2003}, 46--59.
• 26: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
• 27: Gerard J. Holzmann, An Analysis of Bitstate Hashing, Formal Methods in System Design, v.13 n.3, p.289-307, Nov. 1998 [doi>10.1023/A:1008696026254]
• 28: 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]
• 29: Richard Johnsonbaugh , Martin Kalin, A graph generation software package, Proceedings of the twenty-second SIGCSE technical symposium on Computer science education, p.151-154, March 07-08, 1991, San Antonio, Texas, United States
• 30: Eric Y. T. Juan , Jeffrey J. P. Tsai , Tadao Murata, Compositional verification of concurrent systems using Petri-net-based condensation rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.5, p.917-979, Sept. 1998 [doi>10.1145/293677.293681]
• 31: Sascha Konrad , Betty H. C. Cheng, Real-time specification patterns, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062526]
• 32: Larsen, K. G. and Niebert, P., Eds. 2003. Formal Modeling and Analysis of Timed Systems: 1st International Workshop, FORMATS 2003, Revised Papers. Lecture Notes in Computer Science, vol. 2791. Springer.
• 33: Kim G. Larsen , Justin Pearson , Carsten Weise , Wang Yi, Clock difference diagrams, Nordic Journal of Computing, v.6 n.3, p.271-298, Fall 1999
• 34: Larsen, K. G., Pettersson, P., and Yi, W. 1997. Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 1-2, 134--152.
• 35: D. Lugiez , P. Niebert , S. Zennou, A partial order semantics approach to the clock explosion problem of timed automata, Theoretical Computer Science, v.345 n.1, p.27-59, 21 November 2005 [doi>10.1016/j.tcs.2005.07.023]
• 36: Anmol Mathur , Ali Dasdan , Rajesh K. Gupta, Rate analysis for embedded systems, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.3, p.408-436, July 1998 [doi>10.1145/293625.293631]
• 37: Kenneth L. McMillan , David L. Dill, Algorithms for Interface Timing Verification, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.48-51, October 11-14, 1992
• 38: Jesper B. Møller , Jakob Lichtenberg , Henrik Reif Andersen , Henrik Hulgaard, Difference Decision Diagrams, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.111-125, September 20-25, 1999
• 39: Moore, S. K. 2006. Winner: Multimedia monster. IEEE Spectrum. 43, 1, 20--23.
• 40: OMG. 2006. UML resource page. http://www.uml.org/#Links-UML2Tools.
• 41: OMG, T. O. M. G. 2005. Unified modeling language: Superstructure, version 2.0. Tech. rep. formal/05-07-04. August.
• 42: Paul Pop , Petru Eles , Zebo Peng , Traian Pop, Analysis and optimization of distributed real-time embedded systems, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.3, p.593-625, July 2006
• 43: Sawitzki, D. 2004. Experimental studies of symbolic shortest-path algorithms. In Workshop on Experimental Algorithms (WEA'04), C. C. Ribeiro and S. L. Martins, Eds. Lecture Notes in Computer Science, vol. 3059. Springer, 482--497.
• 44: Somenzi, F. 2006. CUDD:CU Decision Diagram Package, Release 2.4.1.
• 45: Christian Stehno, Real-Time Systems Design with PEP, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.476-480, April 08-12, 2002
• 46: Wang, F., Wu, R.-S., and Huang, G.-D. 2005. Verifying timed and linear hybrid rule-systems with red. In International Conference on Software Engineering and Knowledge Engineering (SEKE'05), W. C. Chu, N. J. Juzgado, and W. E. Wong, Eds. 448--454.
• 47: Ti-Yen Yen , Alex Ishii , Al Casavant , Wayne Wolf, Efficient Algorithms for Interface Timing Verification, Formal Methods in System Design, v.12 n.3, p.241-265, April 1, 1998 [doi>10.1023/A:1008680300467]
• 48: Zennou, S., Yguel, M., and Niebert, P. 2003. Else: A new symbolic state generator for timed automata. See Larsen and Niebert {2003}, 273--280.
• 49: W. M. Zuberek, Timed Petri nets and preliminary performance evaluation, Proceedings of the 7th annual symposium on Computer Architecture, p.88-96, May 06-08, 1980, La Baule, United States [doi>10.1145/800053.801913]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

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

General Terms:
Algorithms, Verification

Keywords:
Timing verification, execution scenarios, real time systems, static timing analysis