The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.12 - December (2009 vol.58)
pp: 1640-1653
Ştefan Andrei , Lamar University, Beaumont
Albert Mo Kim Cheng , University of Houston, Houston
ABSTRACT
Embedded and real-time systems are increasingly common and complex, requiring formal specification and verification in order to guarantee their satisfaction of desirable safety and timing requirements. Real-Time Logic (RTL) has been used to capture both the specification (denoted by SP) of a real-time system and the desirable safety assertions (denoted by SA) with respect to this system specification. A verification procedure then determines whether the safety assertions hold with respect to the system specification. However, the satisfiability problem for RTL (i.e., "Can SP \rightarrow SA hold?”), as well as for other first order logics, is undecidable. Consequently, efforts have been focused on identifying nontrivial classes of formulas sufficiently practical for describing industrial real-time systems for which the verification and debugging can be done via efficient heuristics. One such class of formulas is the so-called path RTL. The first contribution of this paper is to extend the existing path RTL class without sacrificing the time complexity of the traditional path RTL heuristic for verification. This implies that we can specify and verify real-time systems, which we were unable to do using the existing path RTL, in the extended path RTL. For real-time systems with large specifications, there is a lot of room for improvement in the algorithms used for verification and debugging. The second contribution of this paper is an efficient method to perform verification and debugging of real-time systems specifications using decomposition techniques. Our idea is to decompose the constraint graph, used in existing approaches, into independent subgraphs so that it is no longer necessary to analyze the entire specification at once, but rather its individual and smaller components. However, none of the above heuristics necessarily finds an “optimal implication.” After verifying SP \rightarrow SA and deploying the system implementing SP, performance changes as a result of power saving, faulty components, and cost saving in the processing platform for the tasks specified in SP affect the computation times of the specified tasks. This leads to a different but related SP, which would violate the original SP \rightarrow SA theorem if SA remains the same. It is desirable, therefore, to determine an optimal SP with the slowest possible computation times for its tasks such that the SA is still guaranteed. This is clearly a fundamental issue in the design and implementation of highly dependable real-time/embedded systems. The third contribution of this paper tackles this fundamental issue by describing a new method for relaxing SP and tightening SA such that SP \rightarrow SA is still a theorem. We have implemented this method in the Java-based DEVO-RTL tool and tested it on several industrial real-time systems. Experimental results show that only about 10 percent of the running time of the heuristic for the verification of SP \rightarrow SA is needed to find an optimal theorem.
INDEX TERMS
Real-time system, system development tool, automatic debugging, timing constraint, counting SAT problem, incremental computation, optimization.
CITATION
Ştefan Andrei, Albert Mo Kim Cheng, "Efficient Verification and Optimization of Real-Time Logic-Specified Systems", IEEE Transactions on Computers, vol.58, no. 12, pp. 1640-1653, December 2009, doi:10.1109/TC.2009.79
REFERENCES
[1] S. Andrei and A.M.K. Cheng, “Faster Verification of rtl-Specified Systems via Decomposition and Constraint Extension,” Proc. 27th IEEE Real-Time Systems Symp., pp. 67-76, 2006.
[2] S. Andrei and A.M.K. Cheng, “Optimization of Real-Time Systems Timing Specifications,” Proc. 12th IEEE Int'l Conf. Embedded and Real-Time Computing Systems and Applications, pp. 68-74, 2006.
[3] F. Jahanian and A. Mok, “Safety Analysis of Timing Properties in Real-Time Systems,” IEEE Trans. Software Eng., vol. 12, no. 9, pp. 890-904, Sept. 1986.
[4] F. Jahanian and A. Mok, “A Graph-Theoretic Approach for Timing Analysis and Its Implementation,” IEEE Trans. Computers, vol. 36, no. 8, pp. 961-975, Aug. 1987.
[5] F. Wang and A.K. Mok, “RTL and Refutation by Positive Cycles,” Proc. Formal Methods Europe Symp., pp. 659-680, 1994.
[6] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. Ninth IEEE Real-Time Systems Symp., pp. 12-21, 1988.
[7] S. Andrei and W.-N. Chin, “Incremental Satisfiability Counting For Real-Time Systems,” Proc. 10th IEEE Real-Time and Embedded Technology and Applications Symp., pp. 482-489, 2004.
[8] A.M.K. Cheng, Real-Time Systems. Scheduling, Analysis, and Verification. Wiley Interscience, 2002.
[9] A.K. Mok, D.-C. Tsou, and R.C.M. de Rooij, “The MSP.RTL Real-Time Scheduler Synthesis Tool,” Proc. 17th IEEE Real-Time Systems Symp., pp. 118-128, 1996,
[10] L.E.P. Rice and A.M.K. Cheng, “Timing Analysis of the X-38 Space Station Crew Return Vehicle Avionics,” Proc. Fifth IEEE-CS Real-Time Technology and Applications Symp., pp. 255-264, 1999.
[11] S. Andrei, W.N. Chin, A.M.K. Cheng, and M. Lupu, “Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting,” IEEE Trans. Computers, vol. 55, no. 7, pp. 830-842, July 2006.
[12] A. Dasdan, “Efficient Algorithms for Debugging Timing Constraint Violations,” Proc. Eighth ACM/IEEE Int'l Workshop Timing Issues in the Specification and Synthesis of Digital Systems, pp. 50-56, 2002.
[13] O. Sokolsky and S. Smolka, “Incremental Model Checking in the Modal Mu-Calculus,” Proc. Int'l Conf. Computer-Aided Verification, 1994.
[14] C.L. Conway, K.S. Namjoshi, D. Dams, and S.A. Edwards, “Incremental Algorithms for Inter-Procedural Analysis of Safety Properties,” Computer Aided Verification, K. Etessami and S.Rajamani, eds., pp. 449-461, Springer-Verlag, 2005.
[15] R. Alur, R. Grosu, I. Lee, and O. Sokolsky, “Compositional Refinement for Hierarchical Hybrid Systems,” Proc. Fourth Int'l Workshop Hybrid Systems: Computation and Control, pp. 33-48, 2001.
[16] I. Shin and I. Lee, “Compositional Real-Time Scheduling Framework,” Proc. Real-Time Systems Symp., pp. 57-67, 2004.
[17] S.S. Kulkarni, J.M. Rushby, and N. Shankar, “A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs,” Proc. IEEE Int'l Conf. Distributed Computing Systems (ICDCS) Workshop Self-Stabilizing Systems, pp. 33-40, 1999.
[18] S. Owre, J.M. Rushby, N. Shankar, and D.W.J. Stringer-Calvert, “PVS: An Experience Report,” Proc. Int'l Workshop Current Trends in Applied Formal Methods—FM-Trends '98, pp. 338-345, 1998.
[19] G.R. Hellestrand, “Systems Architecture: The Empirical Way: Abstract Architectures to ‘Optimal’ Systems,” Proc. Int'l Conf. Embedded Software, 147-158, 2005.
[20] V. Carchiolo, M. Malgeri, and G. Mangioni, “Hardware/Software Synthesis of Formal Specifications in Codesign of Embedded Systems,” Design Automation of Electronic Systems, vol. 5, no. 3, pp.399-432, 2000.
[21] W. Zhao, D. Whalley, C. Healy, and F. Mueller, “Improving WCET by Applying a WC Code Positioning Optimization,” ACM Trans. Architecture and Code Optimization, vol. 2, no. 4, pp. 335-365, 2005.
[22] T.A. Henzinger, C.M. Kirsch, and S. Matic, “Composable Code Generation for Distributed Giotto,” ACM SIGPLAN Notices, vol. 40, no. 7, pp. 21-30, 2005.
[23] P. Pop, P. Eles, and Z. Peng, “Schedulability-Driven Frame Packing for Multicluster Distributed Embedded Systems,” ACM Trans. Embedded Computing Systems, vol. 4, no. 1, pp.112-140, 2005.
51 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool