Difference between revisions of "AspectLTL"

From AspectLTL Wiki Page
Jump to: navigation, search
(Screenshot)
(Demo)
 
(9 intermediate revisions by 2 users not shown)
Line 27: Line 27:
  
 
* AspectLTL plug-in change log:
 
* AspectLTL plug-in change log:
** June 2010 (v1.2.0) First version available
+
** Jun. 2010 (v1.2.0) First version available.
** Feb. 2011 (v1.3.0) Support for traceability and conflict debugging  
+
** Feb. 2011 (v1.3.0) Support for traceability and conflict debugging.
** Mar. 2011 (v1.3.1) Preferences page and few important fixes...
+
** Mar. 2011 (v1.3.1) Preferences page and few important fixes...  ('''requires''' Eclipse 3.6.X).
** June 2011 (v1.3.2) Interactive graphic view of the generated controller, few bug fixes and usability improvements
+
** Jun. 2011 (v1.3.2) Interactive graphic view of the generated controller, few bug fixes and usability improvements.
 
+
** Jan. 2012 (v1.4.0) Migration to Eclipse Indigo. Includes enhanced parsing, enhanced interactive graphic view (including debugging controller), and some bug fixes ('''requires''' Eclipse 3.7.X).
* The Eclipse update site for the AspectLTL plug-in is http://aspectltl.ysaar.net/updatesite/.
+
Note that AspectLTL plugin v1.3.1 and above requires Eclipse Helios 3.6.X (not including Eclipse Indigo 3.7.0).
+
  
 +
Note that there are now two Eclipse update sites for AspectLTL plug-in:
 +
* The update site for AspectLTL plug-in v1.3.2 is http://aspectltl.ysaar.net/updatesite/3.6.X/ ('''Not''' compatible with Eclipse 3.7.X and above).
 +
* The update site for AspectLTL plug-in v1.4.0 is http://aspectltl.ysaar.net/updatesite/3.7.X/ ('''Not''' compatible with Eclipse 3.6.X and below).
  
 
== References ==
 
== References ==
Line 40: Line 41:
 
* S. Maoz and Y. Sa'ar, '''"AspectLTL: An Aspect Language for LTL Specifications"'''.  In Proc. 10th Aspect Oriented Software Development Conf. (AOSD'11), ACM, pp. 19-30, March 2011.  [[Media:aspectltl-aosd11.pdf|paper download]]
 
* S. Maoz and Y. Sa'ar, '''"AspectLTL: An Aspect Language for LTL Specifications"'''.  In Proc. 10th Aspect Oriented Software Development Conf. (AOSD'11), ACM, pp. 19-30, March 2011.  [[Media:aspectltl-aosd11.pdf|paper download]]
  
* S. Maoz and Y. Sa'ar, '''"Two-Way Traceability and Conflict Debugging for AspectLTL Programs"'''.  Submitted.
+
* S. Maoz and Y. Sa'ar, '''"Two-Way Traceability and Conflict Debugging for AspectLTL Programs"'''.  In Proc. 11th Aspect Oriented Software Development Conf. (AOSD'12), ACM, March 2012.  [[Media:aspectltl-tracing-aosd12.pdf|paper download]]
 
+
  
 
== Demo ==
 
== Demo ==
  
{{#evp:youtubehd|eFd2ygmdbw0|AspectLTL Demo Video}}
+
{{#ev:youtube|eFd2ygmdbw0|854x480||AspectLTL Demo Video}}
 +
 
 +
== Screenshots ==
 +
 
 +
A sequence of three screenshots from the AspectLTL plug-in, showing a debugging session of the Printer example (one of the examples supplied with the plug-in).  The screenshots show the selected aspects and base on the left, a textual description of the reversed roles controller, and traceability information in markers attached to the LTLSPEC of the two open aspects.  Finally, on the right, a graph-based view of the reversed roles controller: input (environment) variables values are attached to the edges, and output (system) variables values are attached to the nodes. As this is a reversed roles controller, where the engineer plays the role of the system (i.e., chooses the output), each edge allows to open a popup menu, listing the alternative steps to choose from. 
  
== Screenshot ==
+
[[File:DebugScreenshot1a.png|1000px]]
  
A screenshot from the AspectLTL plug-in, showing a debugging session of the Printer example (one of the examples supplied with the plug-in).  The screenshot shows the selected aspects and base on the left, a textual description of the reversed roles controller, and traceability information in markers attached to the LTLSPEC of the two open aspects.  Finally, on the right, a graph-based view of the reversed roles controller: input (environment) variables values are attached to the edges, and output (system) variables values are attached to the nodes. As this is a reversed roles controller, where the engineer plays the role of the system (i.e., chooses the output), each edge allows to open a popup menu, listing the alternative steps to choose from.
+
[[File:DebugScreenshot1b.png|1000px]]
  
[[File:Screenshot_debug.jpg|1000px]]
+
[[File:DebugScreenshot1c.png|1000px]]

Latest revision as of 07:43, 4 July 2015


AspectLTL is a temporal-logic based language for the specification and implementation of crosscutting concerns.

AspectLTL enables the modular declarative specification of expressive concerns, covering the addition of new behaviors, as well as the specification of safety and liveness properties. Moreover, given an AspectLTL specification, consisting of a base system and a set of aspects, we provide AspectLTL with a composition and synthesis-based weaving process, whose output is a correct-by-construction executable artifact. The language is supported by a prototype tool and is demonstrated using running examples.

AspectLTL was created by Shahar Maoz and Yaniv Sa'ar. It is first presented in the paper: S. Maoz and Y. Sa'ar, "AspectLTL: An Aspect Language for LTL Specifications", AOSD'11.

Resources

  • AspectLTL plug-in change log:
    • Jun. 2010 (v1.2.0) First version available.
    • Feb. 2011 (v1.3.0) Support for traceability and conflict debugging.
    • Mar. 2011 (v1.3.1) Preferences page and few important fixes... (requires Eclipse 3.6.X).
    • Jun. 2011 (v1.3.2) Interactive graphic view of the generated controller, few bug fixes and usability improvements.
    • Jan. 2012 (v1.4.0) Migration to Eclipse Indigo. Includes enhanced parsing, enhanced interactive graphic view (including debugging controller), and some bug fixes (requires Eclipse 3.7.X).

Note that there are now two Eclipse update sites for AspectLTL plug-in:

References

  • S. Maoz and Y. Sa'ar, "AspectLTL: An Aspect Language for LTL Specifications". In Proc. 10th Aspect Oriented Software Development Conf. (AOSD'11), ACM, pp. 19-30, March 2011. paper download
  • S. Maoz and Y. Sa'ar, "Two-Way Traceability and Conflict Debugging for AspectLTL Programs". In Proc. 11th Aspect Oriented Software Development Conf. (AOSD'12), ACM, March 2012. paper download

Demo

AspectLTL Demo Video

Screenshots

A sequence of three screenshots from the AspectLTL plug-in, showing a debugging session of the Printer example (one of the examples supplied with the plug-in). The screenshots show the selected aspects and base on the left, a textual description of the reversed roles controller, and traceability information in markers attached to the LTLSPEC of the two open aspects. Finally, on the right, a graph-based view of the reversed roles controller: input (environment) variables values are attached to the edges, and output (system) variables values are attached to the nodes. As this is a reversed roles controller, where the engineer plays the role of the system (i.e., chooses the output), each edge allows to open a popup menu, listing the alternative steps to choose from.

DebugScreenshot1a.png

DebugScreenshot1b.png

DebugScreenshot1c.png