
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Victor Braberman, Nicolas Kicillof, Alfredo Olivero, "A ScenarioMatching Approach to the Description and Model Checking of RealTime Properties," IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 10281041, December, 2005.  
BibTex  x  
@article{ 10.1109/TSE.2005.131, author = {Victor Braberman and Nicolas Kicillof and Alfredo Olivero}, title = {A ScenarioMatching Approach to the Description and Model Checking of RealTime Properties}, journal ={IEEE Transactions on Software Engineering}, volume = {31}, number = {12}, issn = {00985589}, year = {2005}, pages = {10281041}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.131}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A ScenarioMatching Approach to the Description and Model Checking of RealTime Properties IS  12 SN  00985589 SP1028 EP1041 EPD  10281041 A1  Victor Braberman, A1  Nicolas Kicillof, A1  Alfredo Olivero, PY  2005 KW  Index Terms Requirements/specifications KW  model checking KW  formal methods KW  scenariobased verification. VL  31 JA  IEEE Transactions on Software Engineering ER   
[1] ITUT, “Recommendation Z. 120. Message Sequence Charts,” Technical Report Z120, Int'l Telecomm. Union— Standardization Sector, Genève, 2000.
[2] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property Specifications for FiniteState Verification,” Proc. 21st ACM/IEEE Int'l Conf. Software Eng. (ICSE '99), pp. 411420, 1999.
[3] D. Harel and R. Marelly, “Playing with Time: On the Specification and Execution of TimeEnriched lscs,” Proc. 10th IEEE/ACM Int'l Symp. MASCOTS '02, pp. 193202, 2002.
[4] M.H. Smith, G.J. Holzmann, and K. Etessami, “Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs,” Proc. Fifth IEEE Int'l Symp. Requirements Eng. (RE '01), pp. 1422, 2001.
[5] A. Alfonso, V. Braberman, N. Kicillof, and A. Olivero, “Visual Timed Event Scenarios,” Proc. 26th ACM/IEEE Int'l Conf. Software Eng. (ICSE '04), 2004.
[6] R. Alur, C. Courcoubetis, and D.L. Dill, “ModelChecking in Dense RealTime,” Information and Computation, vol. 104, no. 1, pp. 234, 1993.
[7] B. Alpern and F. Schneider, “Verifying Temporal Properties without Temporal Logic,” ACM Trans. Programming Languages and Systems, vol. 11, no. 1, pp. 147167, 1989.
[8] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183235, 1994.
[9] R. Alur and T.A. Henzinger, “A Really Temporal Logic,” Proc. IEEE Symp. Foundations of Computer Science, pp. 164169, 1989.
[10] T. Wilke, “Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata,” Formal Techniques in RealTime and FaultTolerant Systems, H. Langmaack, W.P. de Roever, and J. Vytopil, eds., pp. 694715, Lbeck: Springer, 1994.
[11] A. Alfonso, V. Braberman, D. Garbervetsky, N. Kicillof, A. Olivero, and F. Schapachnik, “Vintime: Combining HighLevel Finesse with LowLevel Muscle to Verify RealTime Systems,” Proc. PriSE '04, First Conf. PRInciples of Software Eng., 2004.
[12] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “UPPAAL— A Tool Suite for Automatic Verification of RealTime Systems,” Proc. Int'l Conf. Hybrid Systems, pp. 232243, 1995.
[13] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, “Kronos: A ModelChecking Tool for RealTime Systems,” Proc. 10th Int'l Conf. CAV '98, pp. 546550, 1998.
[14] N.F. Maxemchuk and D.H. Shur, “An Internet Multicast System for the Stock Market,” ACM Trans. Computer Systems, vol. 19, no. 3, pp. 384412, 2001.
[15] V. Braberman, N. Kicillof, and A. Olivero, “Visual Timed Event Scenarios,” Technical Report 05011, Computer Science Dept. School of Science, Univ. of Bue nos Aires, 2005.
[16] V. Braberman and M. Felder, “Verification of RealTime Designs: Combining Scheduling Theory with Automatic Formal Verification,” Proc. Seventh ACM/SIGSOFT Int'l Conf. ESEC/FSE '99, pp. 494510, 1999.
[17] V. Braberman, D. Garbervetsky, and A. Olivero, “Improving the Verification of Timed Systems Using Influence Information,” Proc. Eighth Int'l Conf. TACAS '02, pp. 2136, 2002.
[18] S. Uchitel, J. Kramer, and J. Magee, “Negative Scenarios for Implied Scenario Elicitation,” Proc. 10th ACM/SIGSOFT Int'l Conf. FSE '02, pp. 109118, 2002.
[19] N. Amla, E.A. Emerson, and K.S. Namjoshi, “Efficient Decompositional Model Checking for Regular Timing Diagrams,” Proc. Int'l Conf. Correct Hardware Design and Verification Methods, pp. 6781, 1999.
[20] B. Sengupta and R. Cleaveland, “Triggered Message Sequence Charts,” Proc. SIGSOFT FSE, pp. 167176, 2002.
[21] R. Alur and P. Madhusudan, “Decision Problems for Timed Automata: A Survey,” Proc. SFM, M. Bernardo and F. Corradini, eds., pp. 124, 2004.
[22] R. Alur, T. Feder, and T.A. Henzinger, “The Benefits of Relaxing Punctuality,” Proc. Symp. Principles of Distributed Computing, pp. 139152, 1991.
[23] J.F. Raskin and P.Y. Schobbens, “State Clock Logic: A Decidable RealTime Logic,” Proc. HART, O. Maler, ed., pp. 3347, 1997.
[24] L.E. Moser, Y.S. Ramakrishna, G. Kutty, P.M. MelliarSmith, and L.K. Dillon, “A Graphical Environment for the Design of Concurrent RealTime Systems,” ACM Trans. Software Eng. and Methodology, vol. 6, no. 1, 1997.
[25] G.S. Avrunin, J.C. Corbett, and L.K. Dillon, “Analyzing PartiallyImplemented RealTime Systems,” Proc. 18th ACM/IEEE Int'l Conf. Software Eng. (ICSE '97), pp. 228238, 1997.
[26] J. Klose and H. Wittke, “An Automata Based Interpretation of Live Sequence Charts,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), T. Margaria and W. Yi, eds., pp. 512527, 2001.
[27] H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps, “Temporal Logic for ScenarioBased Specifications,” Proc. 11th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '05), 2005.
[28] T. Firley, M. Huhn, K. Diethers, T. Gehrke, and U. Goltz, “Timed Sequence Diagrams and ToolBased Analysis— A Case Study,” Proc. Second Int'l Conf. UML '99, pp. 645660, Oct. 1999.
[29] V. Levin and D. Peled, “Verification of Message Sequence Charts via Template Matching,” Proc. TAPSOFT, M. Bidoit and M. Dauchet, eds., pp. 652666, 1997.
[30] T. Zheng, F. Khendek, and B. Parreaux, “Refining Timed mscs,” Proc. SDL Forum, R. Reed and J. Reed, eds., pp. 234250, 2003.
[31] D. Giannakopoulou and J. Magee, “Fluent Model Checking for EventBased Systems,” Proc. ACM/SIGSOFT Int'l Conf. ESEC/FSE 2003, pp. 257266, Sept. 2003.
[32] A. Alfonso, “Un Lenguaje Visual para la Especificación y Verificación Automática de Requerimientos de Tiempo Real Complejos,” master's thesis, FCEyN. Univ. de Bue nos Aires, 2003.
[33] K. Havelund and G. Rosu, “Synthesizing Monitors for Safety Properties,” Proc. Eighth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '02), pp. 342356, 2002.
[34] V. Braberman, D. Garbervetsky, and A. Olivero, “Obsslice: A Timed Automata Slicer Based on Observers,” Proc. 16th Int'l Conf. ComputerAided Verification (CAV '04), 2004.
[35] R. Alur, L. Fix, and T.A. Henzinger, “EventClock Automata: A Determinizable Class of Timed Automata,” Theoretical Computer Science, vol. 211, nos. 12, pp. 253273, 1999.
[36] A. Bouajjani, Y. Lakhnech, and S. Yovine, “ModelChecking for Extended Timed Temporal Logics,” Proc. Int'l Symp. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT), B. Jonsson and J. Parrow, eds., pp. 306326, 1996.