This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties
December 2005 (vol. 31 no. 12)
pp. 1028-1041
ASCII Text
x 
 
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, vol. 31, no. 12, pp. 1028-1041, December, 2005.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2005.131,
author = {Victor Braberman and Nicolas Kicillof and Alfredo Olivero},
title = {A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties},
journal ={IEEE Transactions on Software Engineering},
volume = {31},
number = {12},
issn = {0098-5589},
year = {2005},
pages = {1028-1041},
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 Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties
IS - 12
SN - 0098-5589
SP1028
EP1041
EPD - 1028-1041
A1 - Victor Braberman,
A1 - Nicolas Kicillof,
A1 - Alfredo Olivero,
PY - 2005
KW - Index Terms- Requirements/specifications
KW - model checking
KW - formal methods
KW - scenario-based verification.
VL - 31
JA - IEEE Transactions on Software Engineering
ER -
 
A major obstacle in the technology-transfer agenda of behavioral analysis and design methods is the need for logics or automata to express properties for control-intensive systems. Interaction-modeling notations may offer a replacement or a complement, with a practitioner-appealing and lightweight flavor, due partly to the subspecification of intended behavior by means of scenarios. We propose a novel approach consisting of engineering a new formal notation of this sort based on a simple compact declarative semantics: VTS (Visual Timed event Scenarios). Scenarios represent event patterns, graphically depicting conditions over traces. They predicate general system events and provide features to describe complex properties not expressible with MSC-like notations. The underlying formalism supports partial orders and real-time constraints. The problem of checking whether a timed-automaton model has a matching trace is proven decidable. On top of this kernel, we introduce a notation to state properties over all system traces: conditional scenarios, allowing engineers to describe uniquely rich connections between antecedent and consequent portions of the scenario. An undecidability result is presented for the general case of the model-checking problem over dense-time domains, to later identify a decidable—yet practically relevant—subclass, where verification is solvable by generating antiscenarios expressed in the VTS{\hbox{-}}{\rm kernel} notation.

[1] ITU-T, “Recommendation Z. 120. Message Sequence Charts,” Technical Report Z-120, 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 Finite-State Verification,” Proc. 21st ACM/IEEE Int'l Conf. Software Eng. (ICSE '99), pp. 411-420, 1999.
[3] D. Harel and R. Marelly, “Playing with Time: On the Specification and Execution of Time-Enriched lscs,” Proc. 10th IEEE/ACM Int'l Symp. MASCOTS '02, pp. 193-202, 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. 14-22, 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, “Model-Checking in Dense Real-Time,” Information and Computation, vol. 104, no. 1, pp. 2-34, 1993.
[7] B. Alpern and F. Schneider, “Verifying Temporal Properties without Temporal Logic,” ACM Trans. Programming Languages and Systems, vol. 11, no. 1, pp. 147-167, 1989.
[8] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.
[9] R. Alur and T.A. Henzinger, “A Really Temporal Logic,” Proc. IEEE Symp. Foundations of Computer Science, pp. 164-169, 1989.
[10] T. Wilke, “Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata,” Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, and J. Vytopil, eds., pp. 694-715, Lbeck: Springer, 1994.
[11] A. Alfonso, V. Braberman, D. Garbervetsky, N. Kicillof, A. Olivero, and F. Schapachnik, “Vintime: Combining High-Level Finesse with Low-Level Muscle to Verify Real-Time 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 Real-Time Systems,” Proc. Int'l Conf. Hybrid Systems, pp. 232-243, 1995.
[13] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, “Kronos: A Model-Checking Tool for Real-Time Systems,” Proc. 10th Int'l Conf. CAV '98, pp. 546-550, 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. 384-412, 2001.
[15] V. Braberman, N. Kicillof, and A. Olivero, “Visual Timed Event Scenarios,” Technical Report 05-011, Computer Science Dept. School of Science, Univ. of Bue nos Aires, 2005.
[16] V. Braberman and M. Felder, “Verification of Real-Time Designs: Combining Scheduling Theory with Automatic Formal Verification,” Proc. Seventh ACM/SIGSOFT Int'l Conf. ESEC/FSE '99, pp. 494-510, 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. 21-36, 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. 109-118, 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. 67-81, 1999.
[20] B. Sengupta and R. Cleaveland, “Triggered Message Sequence Charts,” Proc. SIGSOFT FSE, pp. 167-176, 2002.
[21] R. Alur and P. Madhusudan, “Decision Problems for Timed Automata: A Survey,” Proc. SFM, M. Bernardo and F. Corradini, eds., pp. 1-24, 2004.
[22] R. Alur, T. Feder, and T.A. Henzinger, “The Benefits of Relaxing Punctuality,” Proc. Symp. Principles of Distributed Computing, pp. 139-152, 1991.
[23] J.-F. Raskin and P.-Y. Schobbens, “State Clock Logic: A Decidable Real-Time Logic,” Proc. HART, O. Maler, ed., pp. 33-47, 1997.
[24] L.E. Moser, Y.S. Ramakrishna, G. Kutty, P.M. Melliar-Smith, and L.K. Dillon, “A Graphical Environment for the Design of Concurrent Real-Time Systems,” ACM Trans. Software Eng. and Methodology, vol. 6, no. 1, 1997.
[25] G.S. Avrunin, J.C. Corbett, and L.K. Dillon, “Analyzing Partially-Implemented Real-Time Systems,” Proc. 18th ACM/IEEE Int'l Conf. Software Eng. (ICSE '97), pp. 228-238, 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. 512-527, 2001.
[27] H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps, “Temporal Logic for Scenario-Based 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 Tool-Based Analysis— A Case Study,” Proc. Second Int'l Conf. UML '99, pp. 645-660, 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. 652-666, 1997.
[30] T. Zheng, F. Khendek, and B. Parreaux, “Refining Timed mscs,” Proc. SDL Forum, R. Reed and J. Reed, eds., pp. 234-250, 2003.
[31] D. Giannakopoulou and J. Magee, “Fluent Model Checking for Event-Based Systems,” Proc. ACM/SIGSOFT Int'l Conf. ESEC/FSE 2003, pp. 257-266, 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. 342-356, 2002.
[34] V. Braberman, D. Garbervetsky, and A. Olivero, “Obsslice: A Timed Automata Slicer Based on Observers,” Proc. 16th Int'l Conf. Computer-Aided Verification (CAV '04), 2004.
[35] R. Alur, L. Fix, and T.A. Henzinger, “Event-Clock Automata: A Determinizable Class of Timed Automata,” Theoretical Computer Science, vol. 211, nos. 1-2, pp. 253-273, 1999.
[36] A. Bouajjani, Y. Lakhnech, and S. Yovine, “Model-Checking for Extended Timed Temporal Logics,” Proc. Int'l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), B. Jonsson and J. Parrow, eds., pp. 306-326, 1996.

Index Terms:
Index Terms- Requirements/specifications, model checking, formal methods, scenario-based verification.
Citation:
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, vol. 31, no. 12, pp. 1028-1041, Dec. 2005, doi:10.1109/TSE.2005.131
Usage of this product signifies your acceptance of the Terms of Use.