In no particular order

• Execution
• Visualization

  • Traceability
  • Test
  • Experimentation of different strategies for priority, scheduling

Currently, all classes are generated in the same package.

• A java class extending ExecutableComponent is generated for a component type
• A java class is generated for every library
• A java class is generated for every user-defined type
• An abstract java class extending ExecutableService is generated for every service
• A java class extending the above Abstract class is generated for every service (for testing reasons)
• A java class extending ExecutableLTS is generated for every LTS

• contains a map of named services,
• is initialized using init() which creates its services and calls initState();
• contains methods for checking invariant parts
• can be assigned a Scheduler

The abstract class contains :

• methods for checking pre/post
• a method for every guard
• an abstract method for every transition
• a map of named Channels

The concrete class contains only concrete methods for every transition

A service

• is initialized (by its component) using init() which creates its lts and calls initState();
• can be reset using reset which resets the LTS and calls initState()
• can be started with start()
• can be assigned a Scheduler

contains a map of outGoingTrasitionNames for StateNames contains a map of Communications for transitions

One class only.

More information for type checking

Several classes.

• parameter exchange
• state interrogation
• variable sharing

• traceable solution
• problem of linearisation of the parameters
• no code to execute

  Considered sources

Simple components without compositions

• Boolean,
• Integer,
• String,

  • Set,
  • structs,
  • enum

  and their functions as defined in the kml library which has been ported to Java

• general predicates containing forall or exists

  • Unchanged Expression

  Execution Framework

• Mono component,
• one simple scheduler per service with the following policy

while lts not in final state or not blocked do

• get outgoing transitions whose guards evaluate as true
• randomly pick one (random seed can be set to reproduce choices)
• no variable access policy

• Mono component,
• component scheduler
• Component state access policy

all communication is forwarded to the channels all channels currently are RandomChannels, which do nothing upon receiving information, and return random values upon request