
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Farn Wang, PaoAnn Hsiung, "Efficient and UserFriendly Verification," IEEE Transactions on Computers, vol. 51, no. 1, pp. 6183, January, 2002.  
BibTex  x  
@article{ 10.1109/12.980017, author = {Farn Wang and PaoAnn Hsiung}, title = {Efficient and UserFriendly Verification}, journal ={IEEE Transactions on Computers}, volume = {51}, number = {1}, issn = {00189340}, year = {2002}, pages = {6183}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.980017}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Efficient and UserFriendly Verification IS  1 SN  00189340 SP61 EP83 EPD  6183 A1  Farn Wang, A1  PaoAnn Hsiung, PY  2002 KW  Verification KW  compositional verification KW  modelchecking KW  realtime systems KW  timed automata KW  formal methods KW  software engineering. VL  51 JA  IEEE Transactions on Computers ER   
A compositional verification method from a highlevel resourcemanagement standpoint is presented for densetime concurrent systems and implemented in the tool of SGM (StateGraph Manipulators) with graphical user interface. SGM packages sophisticated verification technology into stategraph manipulators and provides a user interface which views stategraphs as basic dataobjects. Hence, users do not have to be verification theory experts and do not have to trace inside stategraphs to analyze state and path properties to make the best use of verification theory. Instead, users can construct their own verification strategies based on observation on the stategraph complexity changes after experimenting with some combinations of manipulators. Moreover, SGM allows users to control the complexity of stategraphs through iterative stategraphs merging and reductions before they become out of control. Reduction techniques specially designed for the context of stategraph iteration composition and shared variable manipulations are developed and used in SGM. Experiments on different benchmarks to show SGM performance are reported. An algorithm based on group theory to pick a manipulator combination is presented.
[1] M. Abadi and L. Lamport, “An OldFashioned Recipe for Real Time,” Proc. REX Workshop, RealTime Theory in Practice, pp. 127, June 1991.
[2] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. WongToi, “An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness,” Proc. IEEE Int'l Conf. RealTime Systems Symp. (RTSS '92), 1992.
[3] R. Alur, C. Courcoubetis, and D. Dill, “ModelChecking for RealTime Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[4] R. Alur, T.A. Henzinger, and P.H. Ho, “Automatic Symbolic Verification of Embedded Systems,” Proc. IEEE RealTime Systems Symp., 1993.
[5] F. Balarin, “Approximate Reachability Analysis of Timed Automata,” Proc. RealTime Systems Symp. (RTSS '96), pp. 5261, Dec. 1996.
[6] F. Balarin, K. Petty, A.L. SangiovanniVincentelli, and P. Varaiya, “Formal Verification of the PATHO RealTime Operating System,” Procs. 33rd Conf. Decision and Control (CDC '94), Dec. 1994.
[7] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Y. Wang, and C. Weise, “New Generation of UPPAAL,” Proc. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[8] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428439, 1990.
[9] A. Cimatti, F. Clarke, E. Giunchiglia, and M. Roveri, “NuSmv: A Reimplementation of Smv,” Proc. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[10] E. Clarke, O. Grumberg, M. Minea, and D. Peled, “StateSpace Reduction Using PartialOrdering Techniques,“ Int'l J. Software Tools for Technology, vol. 2, no. 3, pp. 279287, 1999.
[11] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[12] C. Daws and S. Yovine, “Reducing the Number of Clock Variables of Timed Automata,” Proc. RealTime Systems Symp., pp. 7381, Dec. 1996.
[13] A.J. Dill, D.L. Drexler, A.J. Hu, and C.H. Yang, “Protocol Verification as a Hardware Design Aid,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors, 1992.
[14] D. Dill, “Timing Assumptions and Verification of FiniteState Concurrent Systems,” Proc. Int'l Conf. ComputerAided Verification, 1989.
[15] E.A. Emerson and A.P. Sistla, “Utilizing Symmetry When ModelChecking under Fairness Assumptions: An AutomataTheoretic Approach,” ACM Trans. Programming Languages and Systems, vol. 19, no. 4, pp. 617638, July 1997.
[16] J.C. Fernandez, “Aldebaran: A Tool for Verification of Communicating Processes,” Technical Report Spectre C14, LGIIMAG Gre noble, 1989.
[17] J.C. Fernandez and L. Mounier, “On the Fly Verification of Behavioral Equivalences and Preorders,” Proc. Third Int'l. Workshop ComputerAided Verification, July 1991.
[18] P. Godefroid and D. Pirottin, “Refining Dependencies Improves PartialOrder Verification Methods,” Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 438449, June 1993.
[19] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for RealTime Systems,” Proc. IEEE Logics in Computer Science, 1992.
[20] I.N. Herstein, Topics in Algebra, second ed. Lexington, Mass.: Xerox College Publishing, 1975.
[21] K. Hoffman and R. Kunze, Linear Algebra, second ed. Englewood Cliffs, N.J.: Prentice Hall, 1971.
[22] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[23] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[24] P.A. Hsiung and F. Wang, “A StateGraph Manipulator Tools for RealTime System Specification and Verification,” Proc. Int'l Conf. RealTime Computing Systems and Applications (RTCSA '98), 1998.
[25] P.A. Hsiung and F. Wang, “UserFriendly Verification,” Proc. 1999 Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols/Protocol Specification, Testing, and Verification (FORTE/PSTV) J. Wu, S.T. Chanson, Q. Gao, eds., Oct. 1999.
[26] IEEE, ANSI/IEEE 802.3, ISO/DIS 8802/3, IEEE CS Press, 1985.
[27] C.N. Ip and D.L. Dill, “Better Verification through Symmetry,” Formal Methods in System Design, vol. 9, 1996.
[28] L. Lamport, “A Fast Mutual Exclusion Algorithm,” ACM Trans. Computer Systems, vol. 5, no. 1, pp. 1–11, 1987.
[29] F. Laroussine and K.G. Larsen, “Compositional Model Checking of Real Time Systems,” Proc. Sixth Int'l Conf. Concurrency Theory (CONCUR '95), pp. 2741, Aug. 1995.
[30] F. Larsen, K. Larsson, P. Petterson, and Y. Wang, “Efficient Verification of RealTime Systems: Compact Data Structure and StateSpace Reduction,” Proc. Int'l RealTime Systems Symp. (RTSS '97), 1997.
[31] K.G. Larsen, P. Petterson, and W. Yi, “Compositional and Symbolic ModelChecking of RealTime Systems,” Proc. 16th IEEE RealTime Systems Symp., pp. 7687, Dec. 1995.
[32] K.G. Larsen, B. Steffen, and C. Weise, “Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints,” Hybrid System III, pp. 604615, 1996.
[33] R. Mateescu and H. Garavel, “XTL: A MetaLanguage and Tool for Temporal Logic ModelChecking,” Procs. Int'l Workshop Software Tools for Technology Transfer (STTT '98), July 1998.
[34] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[35] R. Milner, Communication and Concurrency, PrenticeHall, Englewood Cliffs, N.J., 1989.
[36] H. Miller and S. Katz, “Saving Space by Fully Exploiting Invisible Transitions,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.
[37] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling RealTime Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794804, Sept. 1992.
[38] K. Petty, “The PATHO Operating System and User's Guide,” technical report, Univ. of California, Berkeley, 1993.
[39] A. Tanenbaum, Computer Networks. Prentice Hall, 1988.
[40] S. Tripakis and S. Yovine, “Analysis of Timed Systems Based on TimeAbstracting Bisimulations,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.
[41] F. Wang and P.A. Hsiung, “Automatic Verification on the Large,” Proc. Third IEEE Int'l Symp. High Assurance Systems Eng. (HASE), Nov. 1998.