Live sequence charts - Revision history

Smadar at 07:36, 23 January 2012

2012-01-23T07:36:07Z

Smadar at 07:35, 23 January 2012

2012-01-23T07:35:41Z

Smadar: /* Selected references on LSC */

2010-11-24T11:31:15Z

‎Selected references on LSC

Smadar: /* Selected references on LSC */

2010-11-23T09:32:21Z

‎Selected references on LSC

Smadar at 09:30, 23 November 2010

2010-11-23T09:30:52Z

Shahar.maoz at 09:29, 18 October 2010

2010-10-18T09:29:16Z

Shahar.maoz at 20:32, 17 October 2010

2010-10-17T20:32:12Z

Shahar.maoz at 20:17, 17 October 2010

2010-10-17T20:17:05Z

Shahar.maoz: New page: Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based speci�cation and programming, which extends the partial-order semantics of classical message sequ...

2010-10-17T20:15:21Z

New page: Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based speci�cation and programming, which extends the partial-order semantics of classical message sequ...

New page

Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based speci�cation and programming, which extends the partial-order semantics of classical message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the de�nition of inter-object scenarios that specify, among other things,<br>possible, mandatory, and forbidden behavior.  LSC was introduced by Werner Damm and David Harel in 2001.

An executable semantics for LSCs, termed play-out, was presented by David Harel and Rami Marelly in 2003, together with a tool called Play-Engine.  A translation of LSC into various temporal logics was defined by Hillel Kugler et al. in 2005.   A UML2-compliant variant of LSC was defined by David Harel and Shahar Maoz in 2006.    The language has been the subject of research in the areas of veri�cation and testing , and in the areas of scenario-based execution (playout) and synthesis.  Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.<br>

More about LSC can be found in the references below.

@@ Line 1: / Line 1: @@
 Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based specification and programming, which extends the classical language of message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the definition of inter-object scenarios that specify, among other things, possible, mandatory, and forbidden behavior. LSC was introduced by Damm and Harel in 1999.
-A method for constructing LSCs directly from a pre-prepared GUI, called [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Language_%26_Concepts#Play-In play-in], as well as a method for executing a collection of LSCs, termed [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-Out play-out], were devised by Harel and Marelly in 2003. They also built a tool, called the Play-Engine to support LSCs and these two methods. A translation of LSC into various temporal logics was defined by Kugler et al. in 2005. A UML2-compliant variant of LSC and a compilation technique from LSC into AspectJ were later defined by Harel and Maoz. The language has been the subject of research on verification, testing, and synthesis, in the areas of specification mining and software visualization, and more. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
+A method for constructing LSCs directly from a pre-prepared GUI, called [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Language_%26_Concepts#Play-In play-in], as well as a method for executing a collection of LSCs, termed [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Language_%26_Concepts#Play-Out play-out], were devised by Harel and Marelly in 2003. They also built a tool, called the Play-Engine to support LSCs and these two methods. A translation of LSC into various temporal logics was defined by Kugler et al. in 2005. A UML2-compliant variant of LSC and a compilation technique from LSC into AspectJ were later defined by Harel and Maoz. The language has been the subject of research on verification, testing, and synthesis, in the areas of specification mining and software visualization, and more. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
 More about LSC can be found in the references below and in [http://www.wisdom.weizmann.ac.il/~harel/ Harel's] homepage.

@@ Line 1: / Line 1: @@
 Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based specification and programming, which extends the classical language of message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the definition of inter-object scenarios that specify, among other things, possible, mandatory, and forbidden behavior. LSC was introduced by Damm and Harel in 1999.
-A method for constructing LSCs directly from a pre-prepared GUI, called [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-In play-in], as well as a method for executing a collection of LSCs, termed [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-Out play-out], were devised by Harel and Marelly in 2003. They also built a tool, called the Play-Engine to support LSCs and these two methods. A translation of LSC into various temporal logics was defined by Kugler et al. in 2005. A UML2-compliant variant of LSC and a compilation technique from LSC into AspectJ were later defined by Harel and Maoz. The language has been the subject of research on verification, testing, and synthesis, in the areas of specification mining and software visualization, and more. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
+A method for constructing LSCs directly from a pre-prepared GUI, called [http://www.weizmann.ac.il/mediawiki/playgo/index.php/Language_%26_Concepts#Play-In play-in], as well as a method for executing a collection of LSCs, termed [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-Out play-out], were devised by Harel and Marelly in 2003. They also built a tool, called the Play-Engine to support LSCs and these two methods. A translation of LSC into various temporal logics was defined by Kugler et al. in 2005. A UML2-compliant variant of LSC and a compilation technique from LSC into AspectJ were later defined by Harel and Maoz. The language has been the subject of research on verification, testing, and synthesis, in the areas of specification mining and software visualization, and more. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
 More about LSC can be found in the references below and in [http://www.wisdom.weizmann.ac.il/~harel/ Harel's] homepage.
@@ Line 17: / Line 17: @@
 *S. Maoz, D. Harel and A. Kleinbort, "A Compiler for Multi-Modal Scenarios: Transforming LSCs into AspectJ", ''ACM Trans. on Software Engineering Method''. To appear 2010.
 *S. Maoz and D. Harel, "From Multi-Modal Scenarios to Code: Compiling LSCs into AspectJ", ''Proc. 14th ACM SIGSOFT Symp. on Foundations of Software Engineering'' (FSE'06), Portland, Nov. 2006, pp. 219-230. [http://www.wisdom.weizmann.ac.il/~harel/papers/LSCtoApects.pdf PDF, 212Kb]
 *D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", ''Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design'' (FMCAD 2002), November 2002, pp. 378-398. [http://www.wisdom.weizmann.ac.il/~harel/papers/FMCAD02.pdf PDF, 135Kb]

← Older revision		Revision as of 11:31, 24 November 2010
Line 16:		Line 16:

	*S. Maoz, D. Harel and A. Kleinbort, "A Compiler for Multi-Modal Scenarios: Transforming LSCs into AspectJ", ''ACM Trans. on Software Engineering Method''. To appear 2010.		*S. Maoz, D. Harel and A. Kleinbort, "A Compiler for Multi-Modal Scenarios: Transforming LSCs into AspectJ", ''ACM Trans. on Software Engineering Method''. To appear 2010.
		+
		+	*S. Maoz and D. Harel, "From Multi-Modal Scenarios to Code: Compiling LSCs into AspectJ", ''Proc. 14th ACM SIGSOFT Symp. on Foundations of Software Engineering'' (FSE'06), Portland, Nov. 2006, pp. 219-230. [http://www.wisdom.weizmann.ac.il/~harel/papers/LSCtoApects.pdf PDF, 212Kb]

	*D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", ''Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design'' (FMCAD 2002), November 2002, pp. 378-398. [http://www.wisdom.weizmann.ac.il/~harel/papers/FMCAD02.pdf PDF, 135Kb]		*D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", ''Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design'' (FMCAD 2002), November 2002, pp. 378-398. [http://www.wisdom.weizmann.ac.il/~harel/papers/FMCAD02.pdf PDF, 135Kb]

@@ Line 9: / Line 9: @@
 *D. Harel and R. Marelly, "Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach", ''Software and Systems Modeling'' (SoSyM) 2 (2003), 82-107.  [http://www.wisdom.weizmann.ac.il/~harel/papers/JSM03.pdf PDF, 420Kb]  (the original publication is available at [http://link.springer.de http://link.springer.de] or at [http://link.springerny.com http://link.springerny.com])
-*D. Harel and R. Marelly, ''Come, Let's Play:  Scenario-Based Programming Using LSCs and the Play-Engine'', Springer-Verlag, 2003.
+*D. Harel and R. Marelly, [http://www.wisdom.weizmann.ac.il/~playbook/Updates/ComeLetsPlay.pdf ''Come, Let's Play:  Scenario-Based Programming Using LSCs and the Play-Engine''], Springer-Verlag, 2003.
 *W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts", ''Formal Methods in System Design'' 19:1 (2001), 45-80.  [http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/LSCs.pdf PDF, 260Kb]

@@ Line 1: / Line 1: @@
-Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based specification and programming, which extends the partial-order semantics of classical message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the definition of inter-object scenarios that specify, among other things,possible, mandatory, and forbidden behavior. LSC was introduced by Werner Damm and David Harel in 2001.
+Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based specification and programming, which extends the classical language of message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the definition of inter-object scenarios that specify, among other things, possible, mandatory, and forbidden behavior. LSC was introduced by Damm and Harel in 1999.
-An executable semantics for LSCs, termed play-out, was presented by David Harel and Rami Marelly in 2003, together with a tool called Play-Engine. A translation of LSC into various temporal logics was defined by Hillel Kugler et al. in 2005. A UML2-compliant variant of LSC was defined by David Harel and Shahar Maoz in 2006.  The language has been the subject of research in the areas of verification and testing , in the areas of scenario-based execution (playout) and synthesis, and in the areas of specification mining and software visualization. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
+A method for constructing LSCs directly from a pre-prepared GUI, called [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-In play-in], as well as a method for executing a collection of LSCs, termed [http://www.weizmann.ac.il/mediawiki/playgo/index.php/About_PlayGo#Play-Out play-out], were devised by Harel and Marelly in 2003. They also built a tool, called the Play-Engine to support LSCs and these two methods. A translation of LSC into various temporal logics was defined by Kugler et al. in 2005. A UML2-compliant variant of LSC and a compilation technique from LSC into AspectJ were later defined by Harel and Maoz. The language has been the subject of research on verification, testing, and synthesis, in the areas of specification mining and software visualization, and more. Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.
-More about LSC can be found in the references below and in [http://www.wisdom.weizmann.ac.il/~harel/ David Harel]'s website.
+More about LSC can be found in the references below and in [http://www.wisdom.weizmann.ac.il/~harel/ Harel's] homepage.
 == Selected references on LSC ==
-=== Language definitions ===
+*D. Harel and R. Marelly, "Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach", ''Software and Systems Modeling'' (SoSyM) 2 (2003), 82-107.  [http://www.wisdom.weizmann.ac.il/~harel/papers/JSM03.pdf PDF, 420Kb]  (the original publication is available at [http://link.springer.de http://link.springer.de] or at [http://link.springerny.com http://link.springerny.com])
-*Werner Damm and [http://www.wisdom.weizmann.ac.il/~harel/ David Harel], '''LSCs: Breathing Life into Message Sequence Charts''', ''Formal Methods in System Design'', 19(1): 45-80 (2001).
+*D. Harel and R. Marelly, ''Come, Let's Play:  Scenario-Based Programming Using LSCs and the Play-Engine'', Springer-Verlag, 2003.
-*[http://www.wisdom.weizmann.ac.il/~harel/ David Harel] and [http://www.se-rwth.de/~maoz/ Shahar Maoz], '''Assert and Negate Revisited: Modal Semantics for UML Sequence Diagrams''', ''Software and Systems Modeling'' (SoSyM), 7(2): 237-252 (2008).
+*W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts", ''Formal Methods in System Design'' 19:1 (2001), 45-80.  [http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/LSCs.pdf PDF, 260Kb]
-=== Scenario-based execution (play-out) and synthesis ===
+*D. Harel and S. Maoz, "Assert and Negate Revisited: Modal Semantics for UML Sequence Diagrams", ''Software and System Modeling'' (SoSyM) 7:2 (2008), 237-252. (Early version in ''5th Int. Workshop on Scenarios and State Machines: Models, Algorithms and Tools'' (SCESM'06), 2006, pp. 13-20.) [http://www.wisdom.weizmann.ac.il/~harel/papers/Assert.and.Negate.pdf PDF, 286Kb]
-*[http://www.se-rwth.de/~maoz/ Shahar Maoz], [http://www.wisdom.weizmann.ac.il/~harel/ David Harel], and Asaf Kleinbort, '''A Compiler for Multi-Modal Scenarios: Transforming LSCs into AspectJ''', ''ACM Trans. on Soft. Eng. and Method.'' (TOSEM). Accepted November 2009. To appear.
+*S. Maoz, D. Harel and A. Kleinbort, "A Compiler for Multi-Modal Scenarios: Transforming LSCs into AspectJ", ''ACM Trans. on Software Engineering Method''. To appear 2010.
-*[http://www.se-rwth.de/~maoz/ Shahar Maoz] and [http://www.wisdom.weizmann.ac.il/~harel/ David Harel], '''From Multi-Modal Scenarios to Code: Compiling LSCs into AspectJ''', ''Proc. 14th ACM SIGSOFT Symp. on Foundations of Software Engineering'' (SIGSOFT FSE'06), ACM, 2006, pp. 219-230.
+*D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", ''Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design'' (FMCAD 2002), November 2002, pp. 378-398. [http://www.wisdom.weizmann.ac.il/~harel/papers/FMCAD02.pdf PDF, 135Kb]
-−
-*[http://www.wisdom.weizmann.ac.il/~harel/ David Harel], Hillel Kugler, Rami Marelly, Amir Pnueli, '''Smart Play-out of Behavioral Requirements''', ''Proc. of Formal Methods in Computer Aided Design'' (FMCAD) 2002, pp. 378-398.
-−
-*[http://www.wisdom.weizmann.ac.il/~harel/ David Harel] and Rami Marelly, '''Specifying and executing behavioral requirements: the play-in/play-out approach''', ''Software and Systems Modeling'' (SoSyM), 2(2): 82-107 (2003)

@@ Line 1: / Line 1: @@
 Live sequence charts (LSC) constitute a visual formalism for inter-object scenario-based speci�cation and programming, which extends the partial-order semantics of classical message sequence charts (MSC) mainly by adding universal and existential modalities. It thus allows the de�nition of inter-object scenarios that specify, among other things,<br>possible, mandatory, and forbidden behavior.&nbsp; LSC was introduced by Werner Damm and David Harel in 2001.
-An executable semantics for LSCs, termed play-out, was presented by David Harel and Rami Marelly in 2003, together with a tool called Play-Engine.&nbsp; A translation of LSC into various temporal logics was defined by Hillel Kugler et al. in 2005.&nbsp;&nbsp; A UML2-compliant variant of LSC was defined by David Harel and Shahar Maoz in 2006.&nbsp;&nbsp;&nbsp; The language has been the subject of research in the areas of veri�cation and testing , and in the areas of scenario-based execution (playout) and synthesis.&nbsp; Initial projects that use LSC have been carried out recently in the automotive, telecommunication, and hardware domains.<br>
+<br>
-−
-−
 More about LSC can be found in the references below.