New developer - Step by step

1. get familiar with the software from the perspective of the user:

• browse the AF3 website (http://af3.fortiss.org/)
• run AF3, play with it
• open the examples (available through the menu of AF3)
• look at the help (available through the menu of AF3)

2. It is now time to build a model on your own:

• Let us study the alternating bit protocol
  http://en.wikipedia.org/wiki/Alternating\_bit\_protocol
• Then implement an AF3 model for the sender and the receiver
  components for this protocol with direct communication
  channels between the two (in other words no message can be
  lost during the transmission).
• After having a suitable simulation of this system, replace
  the direct channels with intermediate media components and
  implement a lossy behavior, i.e. messages can get lost during
  transmission.
• Again, validate the proper functioning of the model by simulation.

2 bis. Do the tutorials available at http://af3.fortiss.org/docs/tutorials/

3. Let us now start with the developer material.
Install Eclipse: http://www.eclipse.org/downloads/packages/release/Neon/3.RC3
Choose the Eclipse Modelling Tools.
Then read the following and do the tutorial:
http://eclipsesource.com/blogs/tutorials/emf-tutorial/
This material is not AutoFocus (“AF3”) specific but provides very useful knowledge to understand how many things work.

4. (from now on, all the next tasks are AF3 specific)
get familiar with the developer installation process of AF3:
AF3 Developer Installation with Oomph (Recommended) OR Developer_Installation (Deprecated)
=>you should now have all the code available in Eclipse
many of the following tasks require reading documents, however they all probably benefit from also reading the code in parallel to get a better understanding.

5. Familiarize yourself with the AF3 Development Workflow. There, you will learn to update your workspace, how to create and contribute changes, and how to perform code reviews.

6. read the following code guidelines:
Check-list_for_Code_Reviews
(you probably won’t understand everything since many things require to be familiar with the code in AF3, but still good to browse to get an idea)

7. read the following issue reporting guidelines:
Check-list_for_New_Issues
Related is the bug/issue tracker that you can find here:
https://af3-developer.fortiss.org/projects/af3-phoenix-release
You can also browse it quickly just to get familiar with it.

8. read all the interface files in the following subpackages:

• org.fortiss.tooling.kernel.service
• org.fortiss.tooling.kernel.ui.service

In addition, browse the following material:
AF3_Plugins_Description
Adding_a_new_plugin_project
Tooling_Kernel_Concepts_and_Services
Tooling_Kernel_Plugins_Description
Many of things are now a little bit outdated, no detailed reading is expected, but only browsing:
it is still very useful to get an idea of some of the things happening in AF3 code, indeed the code base is pretty big when one arrives
without knowing it.
We suggest you do the above readings by looking in parallel at the code.
More generally the entry point to all the above documents is there:
Developers_documentation

8. Try to solve the following small exercises:

• change the color of components
• change the icon of components to any icon you would like
• add in the “Model Elements” a new component which contains automatically one input port of type int, so that the user can drag and drop directly a component with one input
• disallow creating a channel between two Boolean ports

9. Add yourself to the various mailing lists:
https://af3-developer.fortiss.org/projects/autofocus3/wiki/MailinglistSubscription%23
And ask your supervisor to be added to the af_build mailing list.

You will now be done with the general AF3 developer general knowledge, the following sections focus more on particular aspects of AF3.
This depends on what your topic and is therefore to be advised by your supervisor.

Requirements (MIRA)

To be done

Formal verification

6. Get familiar with the software from the perspective of the user with a particular focus on formal verification

• browse the AF3 website (http://af3.fortiss.org/)
• run AF3, play with it
• look at the help (available through the menu of AF3)
• open the examples (available through the menu of AF3)

Beware that formal verification functions are rarely called “formal verification” in order not to frighten the user,
however the following words generally means there is formal verification involved: “analyses”, “semantic analyzer”, “reachability analysis”, “A/G”, “assume guarantee”, “contract”, “patterns”, “conformity analysis”
=>each time you see one of these words, play with the functionality

• in particular, pay attention to the “AF3 Tour example” (FileOpen AF3 Example>Load Simple traffic light AF3 tour example)
  and the “A/G, Contracts, Patterns” of the component “TLCSystem”:
  clicking the buttons “Check all” calls the model checker to check the property on the given line.

As of the date these lines are written, many of these functions are buggy/outdated.
So try a little bit to make them work but if they do not, do not waste your time on them and/or ask your supervisor.

7. Get familiar with the connection AF3-NuSMV

* open the “AF3 Tour example” (FileOpen AF3 Example>Load Simple traffic light AF3 tour example)

* navigate to the “A/G, Contracts, Patterns” item of the component “TLCSystem” and open it

* select one line (out of the four in the table) and click the button “Check selected”
=>this does the following:

1. translates the component hierarchy into the model checker “language”
2. translates the property to be checked in Temporal logic
3. out of this, generate a file understandable by the model checker
4. call the model checker on this file
5. wait for the outcome
6. parses the outcome
7. brings the outcome back to AF3 (as “SUCCESS” or “FAIL”), potentially providing a counter-example in case of FAIL

* if you go to Eclipse, you will see some messages on the console explaining what AF3 did, in particular you will see:

1. the name of the file that was given to the model checker
2. the precise command that was run to call the model checker

• now run the same command from a terminal to be sure you know precisely every step of the process
• finally open the file that was generated (there are actually two of them, one with .smv and one with .cmd, the first one is the most important)
  and try to understand what’s in there by comparing it with the components that you have in AF3;
  To understand completely, read the documentation of NuSMV in parallel http://nusmv.fbk.eu/NuSMV/userman/index-v2.html

8. You should now have a good idea of what’s going on in the translation from AF3 to NuSMV.
You can now read the code to see how it’s done.
Browse (“browse” means you have to go through it, but not to spend one hour on every single class, you just need to get an idea of what’s going on)
in particular the code of the following plugins:

• org.fortiss.af3.analyses.ui (only the “src” directory)

deals with the GUI elements that are related to formal verification (I suggest you actually browse this code in parallel with
running AF3 so that you can see which function that you discovered previously matches which precise part of the code).

=>general comment: it is a big plugin, a bit messy, provides lots of functions in a heterogenous way.
That needs a big rewriting, which I will do one day when I get the time :-)
So it can be hard to read, it is criticizable, but for now just focus on trying to understand what’s going on in an approximate way.
The goal is that you are able later on, when I ask you something, to think “oh I’ve seen something related in this plugin I know where to look”.
You can get this way many entry points that will help your future work.

• org.fortiss.af3.analyses/src (only “src/*” and “model/*.ecore” — the latter generates the code in “generated-src/*”)

all the “real work” achieved for formal verification.
Generally all the GUI elements of org.fortiss.af3.analyses.ui are just a facade to some function of this plugin.
The files “*.ecore” in the “model” directory are Ecore models that you got familiar with in the first task.

• you can read in more detail the code in the directory org.fortiss.af3.analyses.modelchecking.af3tonusmv.impl

=>that’s the place where the translation AF3->NuSMV is actually implemented

• org.fortiss.af3.tools (especially the /nusmv directory(/ies))

here is the internal representation of the language of NuSMV (in the model nusmv.ecore), as well as the implementation of the command invocation.

Design Space Exploration

To be adapted to new perspective