Smart Play-out of Behavioral Requirements
作者： David Harel , Hillel Kugler , Rami Marelly , Amir Pnueli
关键词: Model checking 、 Real-time computing 、 Software engineering 、 Formal verification 、 Computer science 、 Temporal logic 、 Circuit design 、 Message sequence chart 、 Reactive system
摘要: We describe a methodology for executing scenario-based requirements of reactive systems, focusing on "playing-out" the behavior using formal verification techniques driving execution. The is implemented in full our play-engine tool. approach appears to be useful many stages development and might also pave way systems that are constructed directly from their requirements, without need intra-object or intra-component modeling coding.
springer.com
weizmann.ac.il 
sci-hub.st 参考文章(34)
Orna Kupfermant, Moshe Y. Vardit, Synthesis with Incomplete Informatio Springer, Dordrecht. pp. 109- 127 ,(2000) , 10.1007/978-94-015-9586-5_6
Rajeev Alur, Gerard J. Holzmann, Doron Peled, An analyzer for message sequence charts tools and algorithms for construction and analysis of systems. pp. 35- 48 ,(1996) , 10.1007/3-540-61042-1_37
David Harel, Michal Politi, Modeling Reactive Systems With Statecharts : The Statemate Approach ,(1998)
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Ramesh Bharadwaj, Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction automated software engineering. ,vol. 6, pp. 37- 68 ,(1999) , 10.1023/A:1008697817793
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan, On Message Sequence Graphs and Finitely Generated Regular MSC Languages international colloquium on automata languages and programming. pp. 675- 686 ,(2000) , 10.1007/3-540-45022-X_57
Amir Pnueli, Elad Shahar, A Platform for Combining Deductive with Algorithmic Verification computer aided verification. pp. 184- 195 ,(1996) , 10.1007/3-540-61474-5_68
Jochen Klose, Hartmut Wittke, An Automata Based Interpretation of Live Sequence Charts tools and algorithms for construction and analysis of systems. pp. 512- 527 ,(2001) , 10.1007/3-540-45319-9_35
Rajeev Alur, Mihalis Yannakakis, Model Checking of Message Sequence Charts CONCUR’99 Concurrency Theory. pp. 114- 129 ,(1999) , 10.1007/3-540-48320-9_10
Marc Lettrari, Jochen Klose, Scenario-Based Monitoring and Testing of Real-Time UML Models Lecture Notes in Computer Science. pp. 317- 328 ,(2001) , 10.1007/3-540-45441-1_24