Sciweavers

Share
NFM
2011
242views Formal Methods» more  NFM 2011»
9 years 3 months ago
Model Checking Using SMT and Theory of Lists
A main idea underlying bounded model checking is to limit the length of the potential counter-examples, and then prove properties for the bounded version of the problem. In softwar...
Aleksandar Milicevic, Hillel Kugler
ENTCS
2006
173views more  ENTCS 2006»
9 years 8 months ago
Concurrent LSC Verification: On Decomposition Properties of Partially Ordered Symbolic Automata
Partially Ordered Symbolic Automata (POSAs) are used as the semantical foundation of visual formalisms like the scenario based language of Live Sequence Charts (LSCs). To check whe...
Tobe Toben, Bernd Westphal
BIRTHDAY
2010
Springer
9 years 9 months ago
On the Power of Play-Out for Scenario-Based Programs
Abstract. We investigate the power of play-out, the execution mechanism associated with scenario-based programming, which was defined as the operational semantics of live sequence ...
David Harel, Amir Kantor, Shahar Maoz
DAGSTUHL
2003
9 years 9 months ago
Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach
The play-in/play-out approach is a method for specifying and developing complex reactive systems. It is built upon a scenariobased philosophy, and uses the language of live sequenc...
David Harel, Hillel Kugler, Gera Weiss
ICSE
2010
IEEE-ACM
9 years 10 months ago
LM: a miner for scenario-based specifications
We present LM, a tool for mining scenario-based specifications in the form of Live Sequence Charts, a visual language that extends sequence diagrams with modalities. LM comes with...
Tuan-Anh Doan, David Lo, Shahar Maoz, Siau-Cheng K...
BIRTHDAY
2008
Springer
9 years 10 months ago
Some Results on the Expressive Power and Complexity of LSCs
Abstract. We survey some of the main results regarding the complexity and expressive power of Live Sequence Charts (LSCs). We first describe the two main semantics given to LSCs: a...
David Harel, Shahar Maoz, Itai Segall
ISSS
2002
IEEE
144views Hardware» more  ISSS 2002»
10 years 29 days ago
A Visual Approach to Validating System Level Designs
This paper proposes a simulation-based methodology for validation of a system under design in an early phase of development. The key element of this approach is the visual speciļ¬...
Jürgen Ruf, Thomas Kropf, Jochen Klose
PADL
2004
Springer
10 years 1 months ago
Symbolic Execution of Behavioral Requirements
Message Sequence Charts (MSC) have traditionally been used as a weak form of behavioral requirements in software design; they denote scenarios which may happen. Live Sequence Chart...
Tao Wang, Abhik Roychoudhury, Roland H. C. Yap, S....
BIRTHDAY
2005
Springer
10 years 1 months ago
Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements
Constructing a program from a speciļ¬cation is a long-known general and fundamental problem. Besides its theoretical interest, this question also has practical implications, since...
David Harel, Hillel Kugler, Amir Pnueli
FASE
2007
Springer
10 years 2 months ago
S2A: A Compiler for Multi-modal UML Sequence Diagrams
We report on S2A, a compiler that translates Modal UML Sequence Diagrams (MSDs), a UML-compliant version of Live Sequence Charts (LSCs), into AspectJ code. It thus provides full co...
David Harel, Asaf Kleinbort, Shahar Maoz
books