This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting
July 2006 (vol. 55 no. 7)
pp. 830-842
ASCII Text
x 
 
Stefan Andrei, Wei Ngan Chin, Albert Mo Kim Cheng, Mihai Lupu, "Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting," IEEE Transactions on Computers, vol. 55, no. 7, pp. 830-842, July, 2006.
 
 
BibTex
x
 
@article{ 10.1109/TC.2006.97,
author = {Stefan Andrei and Wei Ngan Chin and Albert Mo Kim Cheng and Mihai Lupu},
title = {Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting},
journal ={IEEE Transactions on Computers},
volume = {55},
number = {7},
issn = {0018-9340},
year = {2006},
pages = {830-842},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2006.97},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting
IS - 7
SN - 0018-9340
SP830
EP842
EPD - 830-842
A1 - Stefan Andrei,
A1 - Wei Ngan Chin,
A1 - Albert Mo Kim Cheng,
A1 - Mihai Lupu,
PY - 2006
KW - Real-time system
KW - system development tools
KW - automatic debugging
KW - formal methods
KW - timing constraint
KW - counting SAT problem
KW - incremental computation.
VL - 55
JA - IEEE Transactions on Computers
ER -
 
Real-time logic (RTL) [2], [3], [4] is useful for the verification of a safety assertion with respect to the specification of a real-time system. Since the satisfiability problem for RTL is undecidable, the systematic debugging of a real-time system appears impossible. A first step toward this challenge was presented in [1]. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula can help us determine the specific constraints which should be added or modified to get the expected solutions. This paper solves an even more challenging problem specified as future work in [1], namely, the embedding and the integration of our debugger in autonomous systems which generate real-time control plans on-the-fly, since these specifications must meet timing constraints, but without human interaction. The idea is to consider in advance all the necessary information, such as the designer's guidance. We have implemented a tool (called ADRTL) that is able to perform automatic debugging. The confidence of our approach is high as we have successfully evaluated ADRTL on several existing industrial-based applications.

[1] S. Andrei, W.-N. Chin, A. Cheng, and M. Lupu, “Systematic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting,” Proc. 11th IEEE Real-Time and Embedded Technology and Applications Symp., pp. 519-528, 2005.
[2] 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.
[3] 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.
[4] F. Wang and A.K. Mok, “RTL and Refutation by Positive Cycles,” Proc. Formal Methods Europe Symp., pp. 659-680, 1994.
[5] 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.
[6] A. Mok, private communication, Mar. 2005.
[7] 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.
[8] A.M.K. Cheng, Real-Time Systems. Scheduling, Analysis, and Verification. Wiley-Interscience, 2002.
[9] “SDRTL: Systematic Debugging for Path Real-Time Logic,” technical report, School of Computing, Nat'l Univ. of Singapore, May 2004, http://www.comp.nus.edu.sg/~andreiSDRTL.
[10] B. Zupan and A.M.K. Cheng, “Optimization of Rule-Based Systems Using State Space Graphs,” IEEE Trans. Knowledge and Data Eng., vol. 10, no. 2, pp. 238-254, Mar./Apr. 1998.
[11] S. Sodhi and A.M.K. Cheng, “Optimizing Timing Analysis and Verification of Embedded Systems Using Rule-Based-Analytic Techniques,” Proc. WIP Session of IEEE-CS Real-Time Systems Symp., 2003.
[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] 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
[14] 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.
[15] J.N. Hooker, “Solving the Incremental Satisfiability Problem,” J. Logic Programming, vol. 15, pp. 177-186, 1993.
[16] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem-Proving,” Comm. ACM, vol. 5, pp. 394-397, 1962.
[17] J. Whittemore, J. Kim, and K. Sakallah, “SATIRE: A New Incremental Satisfiability Engine,” Proc. 38th ACM/IEEE Conf. Design Automation, pp. 542-545, 2001.
[18] S. Andrei, “The Determinant of the Boolean Formulae,” Analele Universitaţii Bucureşti, Informatica, vol. XLIV, pp. 83-92, 1995.
[19] S. Andrei, “Counting for Satisfiability by Inverting Resolution,” Artificial Intelligence Rev., vol. 22, no. 4, pp. 339-366, 2004.
[20] J.C. Tiernan, “An Efficient Search Algorithm to Find the Elementary Circuits of a Graph,” Comm. ACM, vol. 13, no. 12, pp. 722-726, 1970.
[21] R. Washington, “On-Board Real-Time State and Fault Identification for Rovers,” Proc. IEEE Int'l Conf. Robotics and Automation, pp. 1175-1181, 2000.
[22] R. Volpe, I. Nesnas, T. Estlin, D. Mutz, R. Petras, and H. Das, “The CLARAty Architecture for Robotic Autonomy,” Proc. 2001 IEEE Aerospace Conf., pp. 121-132, 2001.
[23] S. Bayraktar, G.E. Fainekos, and G.J. Pappas, “Experimental Cooperative Control of Fixed-Wing Unmanned Aerial Vehicles,” Proc. 43rd IEEE Conf. Decision and Control, pp. 4292-4298, 2004.
[24] D. Roth, “On the Hardness of Approximate Reasoning,” Artificial Intelligence, vol. 82, pp. 273-302, 1996.
[25] E.M. Clarke and E.A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Proc. IBM Workshop Logics of Programs, pp. 52-71, 1981.
[26] E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach,” ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[27] R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[28] J.R. Burch, E.M. Clarke, and K.L. McMillan, “Symbolic Model Checking: $10^{20}$ States and Beyond,” Information and Computation, vol. 98, no. 2, pp. 142-170, 1992.
[29] K.L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
[30] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193-207, 1999.
[31] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. 36th ACM/IEEE Conf. Design Automation, pp. 317-320, 1999.
[32] S. Andrei and W.-N. Chin, “Incremental Satisfiability Counting for Real-Time Systems,” Technical Report TR-03-04, Faculty of Computer Science, Iaşi University, România, Sept. 2003, http://www.infoiasi.ro/trtr.pl.cgi.
[33] A. Bouajjani, S. Tripakis, and S. Yovine, “On-the-Fly Symbolic Model Checking for Real-Time Systems,” Proc. 18th IEEE Real-Time Systems Symp., pp. 25-34, 1997.
[34] A.M.K. Cheng and S. Fujii, “Self-Stabilizing Real-Time OPS5 Production Systems,” IEEE Trans. Knowledge and Data Eng., vol. 16, no. 12, pp. 1543-1554, Dec. 2004.
[35] K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction,” Proc. 18th IEEE Real-Time Systems Symp., pp. 14-24, 1997.
[36] K.G. Larsen, P. Pettersson, and W. Yi, “UPPAAL: Status and Developments,” Proc. Ninth Int'l Conf. Computer Aided Verification, O. Grumberg, ed., pp. 456-459, 1997.
[37] F. Jahanian and A. Mok, “Modechart: A Specification for Real-Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 12, pp. 933-947, Dec. 1994.
[38] D.A. Stuart, M. Brockmeyer, A.K. Mok, and F. Jahanian, “Simulation-Verification: Biting at the State Explosion Problem,” IEEE Trans. Software Eng., vol. 27, no. 7, pp. 599-617, July 2001.
[39] L.R. Welch, B. Ravindran, B.A. Shirazi, and C. Bruggeman, “Specification and Modeling of Dynamic, Distributed Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., pp. 72-81, 1998.

Index Terms:
Real-time system, system development tools, automatic debugging, formal methods, timing constraint, counting SAT problem, incremental computation.
Citation:
Stefan Andrei, Wei Ngan Chin, Albert Mo Kim Cheng, Mihai Lupu, "Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting," IEEE Transactions on Computers, vol. 55, no. 7, pp. 830-842, July 2006, doi:10.1109/TC.2006.97
Usage of this product signifies your acceptance of the Terms of Use.