SAT solvers

So far, we have been focusing on model checking (post, post), in this post we will start discussing one tool several model checkers use: SAT solvers.

The Boolean Satisfiability Problem (or SAT) is very famous in computer science. Mainly, since it was the first problem to be shown to be NP-complete (a complexity class) but I will not get into complexity in this post.

The problem is to decide whether a given a propositional logic formula is satisfiable or not. A possible (brute force) solution, would be to check every possible assignment for the variables and check whether the formula is satisfied for that assignment. We can see that this solution would imply checking (in the worst case) 2^|VARS| assignments, which as the number of variables increases, the number of checks increases exponentially!

Fortunately, there are many heuristics and algorithms that make SAT feasible in practice for certain inputs even having many many variables. Thus multiple tools are available and are used in the context of formal verification.

For example, SAT solvers are used for Bounded Model Checking (checking the prefixes of the model of length <= k). To translate a state machine over a set of boolean variables V to sat in order to consider k steps, for each variable v in V the variables v_i (i <= k) is created (i.e. the value of variable v in step i) and the initial and transition relation constraints are expressed in terms of step i for every i lower than the bound.

Then by calling the SAT solver, we can check whether some problematic state is reachable (within these k steps).

For example:

if we want to express the first two steps of this state machine (initial and next state), a possible translation could be as follows:

s0_0, s1_0, s2_0, s3_0, s4_0, s5_0: boolean //i.e. the value of each state in step 0
s0_1, s1_1, s2_1, s3_1, s4_1, s5_1: boolean //i.e. the value of each state in step 1
a0, b0, c0: boolean // the value of the variables in step 0
a1, b1, c1: boolean // the value of the variables in step 1

Represent each state at step 0:
assert (s0_0 implies (!a0 and b0 and c0)) // the notation is just to explain the ideas, not the actual input to the sat solver: this assertion indicates which propositions (a, b or c) hold when in s0 at step 0; the ! character represents negation.
assert (s1_0 implies (a0 and b0 and !c0))
assert (s2_0 implies (a0 and !b0 and c0))
assert (s3_0 implies (!a0 and b0 and !c0))
assert (s4_0 implies (!a0 and !b0 and c0))
assert (s5_0 implies (a0 and b0 and c0))

Represent each state at step 1:
assert (s0_1 implies (!a1 and b1 and c1))
assert (s1_1 implies (a1 and b1 and !c1))
assert (s2_1 implies (a1 and !b1 and c1))
assert (s3_1 implies (!a1 and b1 and !c1))
assert (s4_1 implies (!a1 and !b1 and c1))
assert (s5_1 implies (a1 and b1 and c1))

represent the initial states

assert (s0_0 and !s1_0 and !s2_0 and !s3_0 and !s4_0 and !s5_0)

according to the current state at step 0, define the next state

assert (s0_0 implies ((s1_1 or s2_1) and (!s0_1 and !s3_1 and !s4_1 and !s5_1)))
and the same for the remaining states..
assert (s1_0 implies (s3_1 and (!s0_1 and !s1_1 and !s2_1 and !s4_1 and !s5_1)))
...

If we want to check the property:  "if a, then not b and c"

Then we can check for each of the steps, that is:

assert ( (a0 implies not (b0 and c0)) or (a1 implies not (b1 and c1)) )

In this case, the model is satisfiable: for the first two steps it holds that "if a, then not b and c".

If we added two more steps, then when checking:

assert ( (a0 implies not (b0 and c0)) or (a1 implies not (b1 and c1)) or (a2 implies not (b2 and c2)) or (a3 implies not (b3 and c3)) )

the model is shown unsatisfiable.

In the next post I'll explain how to run a sat solver (Minisat) to check these examples

CTL - Computation Tree Logic

In the previous posts we have been talking about Linear Temporal Logic formulas, but there is another kind of temporal logic that allows expressing properties such as "there exists a path starting from  ... ". In CTL (Computation Tree Logic), the temporal operators are the same as in LTL (X, U, G, F), and includes quantifiers (A, E) which express "for every path" or "exists path" respectively.
Then, valid formulas are those that include: Quantifier + Temporal Operator

Examples:
AX p : In every path, the next state satisfies p
EX p : There is a path such that the next state satisfies p

Then the following model:

satisfies the property EX p (there is a path starting from the first state such that in the next state p holds), but it doesn't satisfy AXp (the path that continues below doesn't have p in the next state).

The temporal operators can be combined with boolean ones to build more complex formulas, for example

E(p U AX q) : there is a path where p holds until one state where every next state satisfies q.

Challenge: 

1) for what CTL formula there isn't an LTL equivalent formula ?

2) for what LTL formula there isn't a CTL equivalent formula ?

Interactive nusmv model checking - 3

Continuing with the interactive mode of NuSMV, let's consider our example from the previous posts (nusmv1.smv).

Recall that to enter the interactive mode, we simply execute the application with the -int argument and then build the model (previous post):

NuSMV -int nusmv1.smv

NuSMV > go

Now, in order to start simulating paths, we first choose an initial state (with the pick_state command)

If you don't remember exactly how the commands are called, it is possible to type help and view all the available commands, i.e.

NuSMV > help

and then just to check that is the command we are interested in:

NuSMV > pick_state -h

We can see all the available initial states by passing the argument -i. That is,

NuSMV > pick_state -i

The output looks as follows:

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  request = TRUE
  st = ready


================= State =================
1) -------------------------
  request = FALSE

Choose a state from the above (0-1):

There are two possible states. The first one includes the values for every possible variable, while the second one includes only the valuable of request. This means that the value of st is the same as in the previous state. Let's say we choose the first state which generates a request (i.e. state 0) ).
Now by writing

NuSMV > show_traces -v

The output is

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready

we can simulate randomly other 5 steps:

NuSMV > simulate -r -k 5

<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      request = TRUE
      st = ready
-> State: 1.2 <-
      request = FALSE
      st = busy
-> State: 1.3 <-
      request = TRUE
      st = ready
-> State: 1.4 <-
      request = TRUE
      st = busy
-> State: 1.5 <-
      request = FALSE
      st = ready
-> State: 1.6 <-
      request = TRUE
      st = ready

or we can be asked to interactively select the next k steps (in the example 2 steps)

NuSMV > simulate -i -k 2

So, -r represents choosing randomly, -i interactively and -k the number of steps.

An additional useful option for this command is -c which allows adding constraints that must be satisfied by the next steps. For example, we can start a new simulation path, and the condition we require is that there is a request:

NuSMV > pick_state -r -c "request"

These are the main commands and options I use for simulating paths in a model, for more options, it is always possible to use the help command (get all available commands), command -h (prints the options for any command) or revise the documentation on the site of NuSMV.

Interactive nusmv model checking - 2

Continuing from the last post and the model example, where we could check some LTL formulas, and see the traces, we know show how to apply interactive simulation.
This is useful for when we want to analyze different paths, and see what happens at each step, and what are the possible values of each variable at each step.

For example, we want to step over each step of a trace interactively, choosing the next step at each step.

To run NuSMV in the interactive mode we add the -int option, i.e.
NuSMV -int nusmv1.smv

Then, the NuSMV prompt appears:

NuSMV >

From now on, we will write the commands next to the prompt, but you dont need to write the prompt, just what appears after the > symbol.

The first step is to tell NuSMV to build the model, which is achieved with the command go

NuSMV > go

And now, we can check different properties. For instance:

NuSMV > check_ltlspec -p "G (st = ready -> X st = busy)"

outputs the counterexample while

NuSMV > check_ltlspec -p "G ((st = ready & request) -> X st = busy)"

outputs that the property holds:

-- specification  G ((st = ready & request) ->  X st = busy)  is true

we can check more information about the check_ltlspec option by typing

NuSMV > check_ltlspec -h

which outputs the different options for this command.

Then, we see that for a file that includes some LTL specification properties, we can check the property by number, for instance

NuSMV > check_ltlspec -n 0

To quit the command is "quit"

NuSMV > quit

In the next post I will write about simulating paths within the interactive mode.

valgrind

In this post, I'm going to present a small program written in C and show how to use a tool (Valgrind [1]) to understand the memory access problems.

Let's consider the following program:

main.c:

 #include <stdlib.h>
  void f(void)
  {
     int* x = malloc(10 * sizeof(int));
     x[10] = 0;        // problem 1: heap block overrun
  }                    // problem 2: memory leak -- x not freed

  int main(void)
  {
     f();
     return 0;
  }

Once the program has been compiled (with debug info (-g) into ./main in unix-based systems), we can check for memory issues by running valgrind:

valgrind --leak-check=yes ./main

The output is the following (after the header):

==3938== Invalid write of size 4
==3938==    at 0x40054B: f (main.c:6)
==3938==    by 0x40055B: main (main.c:11)
==3938==  Address 0x51fd068 is 0 bytes after a block of size 40 alloc'd
==3938==    at 0x4C2AB80: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==3938==    by 0x40053E: f (main.c:5)
==3938==    by 0x40055B: main (main.c:11)
==3938==
==3938==
==3938== HEAP SUMMARY:
==3938==     in use at exit: 40 bytes in 1 blocks
==3938==   total heap usage: 1 allocs, 0 frees, 40 bytes allocated
==3938==
==3938== 40 bytes in 1 blocks are definitely lost in loss record 1 of 1
==3938==    at 0x4C2AB80: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==3938==    by 0x40053E: f (main.c:5)
==3938==    by 0x40055B: main (main.c:11)
==3938==
==3938== LEAK SUMMARY:
==3938==    definitely lost: 40 bytes in 1 blocks
==3938==    indirectly lost: 0 bytes in 0 blocks
==3938==      possibly lost: 0 bytes in 0 blocks
==3938==    still reachable: 0 bytes in 0 blocks
==3938==         suppressed: 0 bytes in 0 blocks

The prefix "==3938== " represents the process id.

The first main issue is the invalid write: the first part of the output indicates where the write occurs, while the second part indicates where the memory incorrectly written has been allocated. From this information, we can see that the write within f() is invalid and observe that the problem is because x receives memory for 10 ints (i.e. the accessible indexes are between 0 and 9). Thus, the problem is trying to write to x[10].

The second issue is the memory lost indicated both in the sentence : "40 bytes in 1 blocks are definitely lost in loss record 1 of 1"
and in the LEAK SUMMARY. We can see here which malloc wasn't freed (then one in f (main.c:5)).


We can write now the following similar program:

 #include <stdlib.h>

  void f(void)
  {
     int* x = malloc(10 * sizeof(int));
     x[9] = 0;        // problem 1: we now write to a valid inded
     free(x);       // problem 2: solved, now x was freed
  }


  int main(void)
  {
     f();
     return 0;
  }

and running valgrind we obtain the following output (after the general header):

==4060== HEAP SUMMARY:
==4060==     in use at exit: 0 bytes in 0 blocks
==4060==   total heap usage: 1 allocs, 1 frees, 40 bytes allocated
==4060==
==4060== All heap blocks were freed -- no leaks are possible

The program has no memory issues!

[1] http://valgrind.org/ . The example is from the the tool's quick start guide.

Interactive nusmv model checking - 1

In the last post we saw about model checking LTL formulas with NuSMV by writing the model, the formula to be satisfied, and calling the program from the command line. We will now see a few things useful to interact with the model.

if we run NuSMV with the option -int, NuSMV remains open to ask commands.

We can execute:

NuSMV -int nusmv1.smv

After the header including the NuSMV version, the prompt appears:

NuSMV >

In the next lines this prompt (NuSMV > ) will appear to show where the commands go, but you don't have to write it. We can now write go so that the model is built. That is,

NuSMV > go

And now we can check formulas. For example,

NuSMV > check_ltlspec -p "G st = ready"

outputs a counterexample, while

NuSMV > check_ltlspec -p "st = ready"

indicating that in the first state st is ready, is true.

NuSMV > show_traces 1

shows the first trace (the counterexample to "G st = ready"

At any moment we can use

NuSMV > help
to  see all the available commands

and command -h  to see the options of a command for instance

NuSMV > check_ltlspec -h

Finally we use the quit command to exit.

NuSMV > quit

First NuSMV model check

There are several tools to apply check LTL formulas (LTL - 3, etc.). Among these, NuSMV is an open source tool that I have been using. This tool uses BDDs or SAT solvers to check properties, but I'll leave these topics for later and now focus on actual model checking a system..

In the tutorial, the following example is given:

MODULE main
VAR
request: boolean;
st: {ready, busy};
ASSIGN
init(st) := ready;
next(st) := case
              st = ready & request : busy;
              TRUE : {ready, busy};
            esac;

The given model contains two variables: request is a boolean and st - representing the state of the system - has two possible values (ready or busy).

In the ASSIGN section the initial and transition relation constraints are defined. The variable st is initialized as ready, and then for each transition:
if in the current state st is ready and there is a request, in the next state the value of st will be busy. Otherwise ("TRUE : ..."), the next value of st will be either ready or busy, non-deterministically chosen.
There are no constraints regarding initial or next values of request.

This model represents the given state machine:

The two states on the left are the initial states, since these are the states satisfying that initially st = ready.
Then, almost every transition is possible, besides when st = ready and there is a request, according to the state machine definition in the next state st must be busy.

We can check the following LTL formula:
\(\textbf{G} (st = ready \implies \textbf{X}\ st = busy)\)

That is, at any state, if st = ready, then in the next state st = busy.

To do so, we add the following to the model:

LTLSPEC
G (st = ready -> X st = busy)

Let's assume we have a file  nusmv1.smv (open with any text editor).

Now (from the command line) we can run NuSMV and check if the guarantee holds.

After having downloaded it, we can execute

NuSMV nusmv1.smv

You may need to access the whole path, for instance (in Windows)

C:\Program Files\NuSMV\bin\NuSMV nusmv1.smv

The output is the following:

-- specification  G (st = ready ->  X st = busy)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  request = 1
  st = ready
-> Input: 1.2 <-
-> State: 1.2 <-
  request = 0
  st = busy
-- Loop starts here-> State: 1.3 <-
  st = ready
-> State: 1.4 <--> Input: 1.5 <-
-> State: 1.5 <-
  st = busy
-> Input: 1.6 <-
-> State: 1.6 <-
  st = ready

In the first state of the counterexample, request is true (1) and st is ready. In the next state request is false and st is busy. So far the formula holds.
Then it is inidicated the start of the loop. This is since infinite paths are analyzed, and every counterexample includes a prefix and a loop. The first state of the loop (State 1.3) changes the value of st but not of request (only the variables changed appear). So in State 1.3 request is false and st=ready. However, in the next state st keeps being ready! Our formula is false, since there could be states when the state is ready but the next state is not busy (for instance, when there is no request).

If we change the formula and check

LTLSPEC
G ((request & st = ready) -> X st = busy)

The output obtained is:

-- specification  G ((request & st = ready) ->  X st = busy)  is true

LOTOS - Choice

Some time ago, I've written about the basic events in LOTOS specification (LOTOS - 1). These are given by
g?var: T \(\rightarrow\) an input of type T is expected through the gate g.
g! constant \(\rightarrow\)  an output (constant) is exposed through the gate g.

Additional operators allow building more complex processes:

Sequential composition (;)

Several events can occur in a sequence. For example, g? x: int; g!x+1 represent two events (at two different instants of time). In the first one, it is expected to synchronize on an integer input, while in the second one it is expected to synchronize on the output that is the value received plus one.

We can now define a process P with a gate g that it always receives a value and exposes the value incremented:

process P[g] =
g?x:int ; g!x+1; P[g]

The last element in the sequential composition (P[g]) indicates that a new instance of the process starts when reaching to this point.

Choice ([])

The operator Choice ([]) allows representing the choice between two (or more) paths.

For example,

g! "hello"
[]
g! "world"

allows either exposing "hello" or "world" through the gate g.

Guards ([condition] \(\rightarrow\))

In general, choice conditions are non-deterministic (or more precisely, dependent on the environment). To add conditions, we can use guards combined with the choice operator:

[condition1] \(\rightarrow\) behavior1
[]
[condition2] \(\rightarrow\) behavior2

Then, the behaviors enabled depend on the conditions. For example, let P be a process having been instantiated with a variable x

P[g](x: int)
[x <0] \(\rightarrow\) g! -x; g? y: int; P[g](y)
[]
[x >= 0] \(\rightarrow\) g! x; g? y: int; P[g](y)

This process has an if-else like behavior. It exposes the absolute value of x, receives a new value from the environment (y), and creates a new instance of the process with this value.

Temporal Logic - LTL - 3

In this post we'll see the formal semantics of LTL (LTL - 1, LTL - 2, LTL - Literature):

The model is represented by \(\langle S, I, R, L\rangle\) where \(S\) is the set of states, \(I \subseteq S\) is the set of initial states, \(R:SxS\) is the relation transition definition and \(L: S \rightarrow 2^{AP}\) is the labeling definition where AP is the set of available atomic propositions.

In the example of the last post:

We have three states, \(S = \{s_0,s_1,s_2\}\), with \(I = \{s_0\}\), \(R = \{(s_0,s_1), (s_1,s_2), (s_2, s_2)\}\), \(L = \{s_0\mapsto\{p\},s_1\mapsto\{q\},s_2\mapsto\{p,q,r\}\}\).

A path is an infinite path \(\pi=\pi_0\pi_1\dots\) where  \(\pi_0 \in I\) and for every \(i\), \((\pi_i,\pi_{i+1})\in R\). That is, the first state of the path is an initial state of the model, and for every two consecutive states of the path, there is a relation between them.

Now we define the semantics for the boolean operations and the temporal operators we have mentioned.

\(\pi,i\vDash q\) with \(q \in AP\) if and only if \(q \in L(\pi_i)\). That is, given a path \(\pi\) and index \(i\) of a state within the path an atomic proposition \(q\) is satisfied if and only if \(q\) belongs to the labels of that state.

\(\pi,i\vDash \neg \varphi\) if and only if  \(\pi,i\not\vDash  \varphi\). That is, not a formula is satisfied if the formula itself is not satisfied.

\(\pi,i\vDash  \varphi \land \theta\) if and only if  \(\pi,i\vDash  \varphi\) and \(\pi,i\vDash  \theta\). That is, the conjunction of two linear temporal logic formulas \(\varphi,\theta\) is satisfied if and only if both formulas are satisfied.

\(\pi,i\vDash  \varphi \lor \theta\) if and only if  \(\pi,i\vDash  \varphi\) or \(\pi,i\vDash  \theta\). That is, the disjunction of two linear temporal logic formulas \(\varphi,\theta\) is satisfied if and only at least one of the formulas is satisfied.

Now, we show the semantics of the temporal operators G, F, X, U.

\(\pi,i\vDash \textbf{G}\varphi\) if and only if for every \(j\ge i\), \(\pi,j\vDash \varphi\) , that is, every path starting with every state after \(i\) satisfies \(\varphi\).

\(\pi,i\vDash \textbf{F}\varphi\) if and only if exists \(j\ge i\), \(\pi,j\vDash \varphi\) , that is, there is a state in the future such that the path starting with that state satisfies \(\varphi\).

\(\pi,i\vDash \textbf{X}\varphi\) if and only if \(\pi,i+1\vDash \varphi\) , that is, there is the next state satisfies \(\varphi\).

\(\pi,i\vDash \varphi\textbf{U}\theta\) if and only if exists \(j\ge i\), \(\pi,j\vDash \theta\) and for every \(i\le k < j\), \(\pi,k\vDash \varphi\) , that is, there is a state \(j\) in the future such that the \(\theta\) is satisfied, and every state till \(j\) (non-including) satisfies \(\varphi\).


Or semantics:

Meeting of the Sussex Border Path with Hook Street at Monckton Hook (Andy Potter) / CC BY-SA 2.0

Temporal Logic in Literature

In this post I want to put some phrases from Literature and show (possible) translation to temporal logic (LTL - 1, LTL - 2).

1)
"In such terms Mr Gradgrind always mentally introduced himself, whether to his private circle of acquaintance, or to the public in general." Charles Dickens, Hard Times, Chapter 2

Let's compare these two formulas:

\(F (MrGradgrindMentallyIntroducesHimself)\)

\(G (MrGradgrindMentallyIntroducesHimself)\)

The first one indicates that there is one state in the future in which Mr. Gradgrind mentally introduces himself. The second one indicates that this occurs at every state, matching the keyword always in the sentence.

2)
"There will be the noise of the blows of the whip, which they will give to the horses." Alexandre Dumas, The forty-Five Guardsmen, Chapter 1

Let's compare these two formulas:

\(F\ noiseBlowsOfWhip \land F\ whipToHorses\)

\(F (noiseBlowsOfWhip \land whipToHorses)\)

The first one indicates that there is a state in the future in which there is the noise of the blows of the whip, and there is state in the future in which they whip the horses, while the second one indicates a state in the future in which both things occur. Since we know that both things are related, the whip causes the noise, we know they must be at the same state, and the second formula is preciser.

3)
' This proposal met with general applause, until an old mouse got up and said: "That is all very well, but who is to bell the Cat?" ' Aesop, Aesop's fables, Belling the Cat

A first attempt could to be to write the following formula:

\(Applause \land OldMouseQuestion\)

However, this formula expresses that at the first instant of time both things occur, and the applause may happen later and even later the question. Thus, we may attempt to correct the formula as follows:

\(Applause \land F\ OldMouseQuestion\)

It is better in that it expresses that first the applause occurs and sometime in the future the question by the old mouse. However, the applause goes only to be interrupted by the old mouse (keyword: until). Then we correct it as follows:

\(Applause\ U\ OldMouseQuestion\)

Here represents that the applause goes on until the old mouse asks its question. The only ambiguous part that remains is whether the story starts with the applause or this happens at some moment in the future. Due to our additional knowledge that first there is a discussion, then the proposal to bell the cat and only then the applause, we know that this part does not occur at the first state:

\(F\ Applause\ U\ OldMouseQuestion\)

Modularity 2015 - Submissions: October 10, 2014

Modularity 2015 second round submission deadline: October 10th, 2014

More information: Modularity 2015 - Research Results Track

PSC track submission deadline: 26th September

PSC (Programming for Separation of Concerns) Track of ACM Symposium on Applied Computing deadline: September 26th.

Details on the CFP at http://www.dmi.unict.it/~tramonta/sac/

Temporal Logic - LTL - 2

In the previous post (LTL - 1), we started talking about Linear Temporal Logic, a logic that allows expressing temporal properties about every path of a model.
In particular we have observed the temporal operators (or modalities):
G (Globally)
F (Eventually)
There is a relation between these two operators: Writing that globally something (property) holds, is equivalent to saying that the negation of the property will never hold. In terms of the operators this is expressed as:
G property = not F not property
I take this opportunity to present syntax notations I will use in future posts:
not = \( \neg \)
or = \( \lor \)
and = \( \land \)
Now, other temporal operators of interest are:
X formula (at the next state formula holds)
formula1 U formula2 (formula1 holds until formula2 holds)
For example,

In the given state machine, p q and r are atomic propositions. For example, p could represent x = 1 , q represent y > 0, and r represent that z is within some range of values. These are just examples, for each system, the set of atomic propositions is defined, and with these, the state machine representing the system is built. We will consider that if an atomic proposition does not appear in a state, then that atomic proposition does not hold at that state. For example the first state satisfies \( p \land \neg q \land \neg r \).

When standing at the first state of the model in the example (let's call it M), we can see that the next state satisfies q. That is, \( M \vDash \textbf{X}\ q \). When writing that the model satisfies an LTL formula, we are saying that every path starting from the initial states of the model satisfies the formula.

We can also observe that \(M \vDash  \textbf{X}\ \neg p \) ,\( M \vDash   \neg \textbf{X}\ r \), \( M \vDash  \textbf{X} \textbf{X}\ q \), and \( M \vDash  \textbf{X} \textbf{X}\textbf{X}\ p \). Question to the reader: why?


Thus, X expresses at the next state (from the state we are currently at). For example although the model does not satisfy that at the next state of every path starting from the initial states p will hold, there exists a future state such that its next state will satify p. That is \( M \vDash \textbf{F}\textbf{X}\ p \). And this way the different temporal operators can be combined.

cc license from origin

The remaining operator for this post is U: The idea is that a formula "formula1 U formula2" is satisfied when formula1 holds at every state until some state where formula2 holds. If formula2 holds, then the formula with until holds. If formula2 never holds, then the until formula is not satisifed. In the next blog we will give the more formal definitions of the temporal operators (or modalities) and understand why the express the general idea we have seen in these two posts.

Temporal Logic - LTL - 1

Temporal logic allows expressing properties that a system should satisfy along time. We will first talk about linear temporal logic which expresses properties over every possible path. For example, let's consider the following model:

Let r be the proposition representing that the system is running and h the proposition representing the the system has halted.

Then we could check whether it always holds that this system will always halt. According to the state machine representation this is false: We can consider the path r,r,r,r,... and never get to the halt state.

With linear temporal logic we can express the property "the system will always halt" and other properties referring to time.

For example, the operator G formula (globally) indicates that from a given state, every state state satisfies formula (formula can be any linear temporal logic formula.

For instance, the formula G (r or h) is true. Every state of every path starting from the initial state satisfies that r or h hold. However, the formula G r is not satisfied by every path.

The operator F formula indicates that formula will be true at some state in the future.

The given example does not satisfy F h (because of the given counterexample where the second state is not reached..

However the formula F r, holds (a state satisfying r is reached at the first state)

In future posts we will consider some other examples and other operators.

Call for papers: Modularity 2015

Modularity 2015

 Call for Papers: Modularity '15 Research Results

         March 16-19, 2015, Ft. Collins, Colorado, USA

First round due date: August 4, 2014. Second round due date: October 10, 2014.

Modularity is a key property for scalability of software processes, including debugging, maintenance, reasoning, and testing. Modularity influences system diversity, dependability, performance, evolution, the structure and the dynamics of the organizations that produce systems, human understanding and management of systems, and ultimately system value. Yet the nature of and possibilities for modularity, limits to modularity, the mechanisms needed to achieve it in given forms, and its costs, benefits, and tradeoffs remain poorly understood. Significant advances in modularity thus are possible and promise to yield breakthroughs in our ability to conceive, design, develop, validate, integrate, and evolve modern information systems and their underlying software artifacts.

Modularity at the semantic as well as the syntactic level is a key enabler for the expression of high quality software systems. One of the most important techniques for complexity reduction is abstraction. Novel concepts and abstraction mechanisms, including but not limited to aspect-oriented techniques, are a focus point for improvements in the support for modularity. The scope of this effort covers all perspectives on software systems in all their life-cycle phases, for instance application domain analysis, programming language constructs, formal proofs of system properties, program state visualization in debuggers, performance improvements in compiler algorithms, etc. As the premier international conference on modularity, Modularity'15 continues to advance our understanding of these issues and the expressive power of known techniques.

The Modularity'15 conference invites full, scholarly papers of the highest quality on new ideas and results. Papers are expected to contribute significant new research results with rigorous and substantial validation of specific technical claims, based on scientifically sound reflections on experience, analysis, experimentation, or formal models. Compelling new ideas are especially welcome, which means that the requirements in the areas of validation and maturity are higher for papers that contribute more incremental results.

Modularity'15 is deeply committed to publishing works of the highest caliber. To this aim, two separate paper submission deadlines and review stages are offered. A paper accepted in any round will be published in the proceedings and presented at the conference. Promising papers submitted in the first round that are not accepted may be invited to be revised and resubmitted for review by the same reviewers in the second round. Authors of such invited resubmissions are asked to also submit a letter explaining the revisions made to the paper to address the reviewers' concerns. While there is no guarantee that an invited resubmission will be accepted, this procedure (similar to major revisions requested by journals) is designed to help authors of promising work get their papers into the conference. Submission to both rounds is open for all, and authors who submit to the first round may of course choose to resubmit a revised version in the second round without such an invitation, in which case new reviewers may be appointed. Finally, the same paper cannot be simultaneously submitted to other conferences or journals. In case of doubt, please contact the Program Chair.

Research Topics

Modularity'15 is looking for papers in all areas of software modularity. Topics of interest include, but are not limited to, the following:

* Varieties of modularity: Context orientation; feature orientation; generative programming; aspect orientation; software product lines; traits; families of classes; meta-programming and reflection; components; view-based development.

* Programming languages: Support for modular abstraction in: language design; verification, specification, and static program analysis; compilation, interpretation, and runtime support; formal languages and calculi; execution environments and dynamic weaving; dynamic languages; domain-specific languages.

* Software design and engineering: Requirements and domain engineering; architecture; synthesis; evolution; metrics and evaluation; empirical studies of existing software; economics; testing and verification; semantics; composition and interference; traceability; methodologies; patterns.

* Tools: Crosscutting views; refactoring; evolution and reverse engineering; aspect mining; support for new language constructs.

* Applications: Data-intensive computing; distributed and concurrent systems; middleware; service- oriented computing systems; cyber-physical systems; networking; cloud computing; pervasive computing; runtime verification; computer systems performance; system health monitoring; enforcement of non-functional properties.

* Complex systems: Works that explore and establish connections across disciplinary boundaries, bridging to such areas as biology, economics, education, infrastructure such as buildings or transport systems, and more.

* Composition. Component-based software engineering; Composition and adaptation techniques; Composition algebras, calculi, and type systems; Model-driven composition; Dynamic composition and reconfiguration; Large-scale component-based systems; Cloud, service-oriented architectures; Business process orchestration; Visual composition environments; Performance optimization of composite systems.

Important Dates

* First round:

Submission: August 4, 2014 (23:59 Baker Island / UTC-12)

Notification: September 14, 2014

* Second round:

Submission: October 10, 2014 (23:59 Baker Island / UTC-12)

Notification: December 7, 2014

* Camera ready: February 15, 2015

Submission Guidelines

Modularity'15 is deeply committed to eliciting works of the highest caliber. To this aim, two separate paper submission deadlines and review stages are offered. A paper accepted in any round will be published in the proceedings and presented at the conference. Promising papers submitted in the first round that are not accepted may be invited to be revised and resubmitted for review by the same reviewers in the second round. Authors of such invited resubmissions are asked to also submit a letter explaining the revisions made to the paper to address the reviewers' concerns. While there is no guarantee that an invited resubmission will be accepted, this procedure (similar to major revisions requested by journals) is designed to help authors of promising work get their papers into the conference. Submission to both rounds is open for all, and authors who submit to the first round may of course choose to resubmit a revised version in the second round without such an invitation, in which case new reviewers may be appointed. Finally, the same paper cannot be simultaneously submitted to other conferences or journals. In case of doubt, please get in touch with the Program Chair.

All submissions must conform to both the ACM Policy on Prior Publication and Simultaneous Submissions and the SIGPLAN Republication Policy.

Papers are to be submitted electronically to CyberChair.

Please use http://cyberchairpro.borbala.net/modularitypapers/submit/ to submit your paper. Submissions should use the SIGPLAN Proceedings Format using 9 point font. Please include page numbers in your submission as this will be helpful for the reviewers and also for you when reading their reviews. (If your submission is written using LaTeX, please set the preprint option in the LaTeX \documentclass command to generate page numbers.) Please also ensure that your submission is legible when printed on a black and white printer. In particular, please check that colors remain distinct and font sizes are legible.

To ensure that papers stay focused on their core contributions, the main part of the paper should be no longer than 12 pages. There is a 4 page limit for appendices, and, therefore, for the overall submission must be less than 16 pages. If the paper is accepted, the final submission will be limited to 16 pages, including appendices.

However, it is the responsibility of the authors to keep the reviewers interested and motivated to read their submission. Reviewers are under no obligation to read all or even a substantial portion of a paper if they do not find the initial part of the paper compelling. The committee will not accept a paper if it is unclear that the paper will fit in the Modularity'15 Proceedings.

All submitted papers are peer-reviewed. Accepted papers from all tracks will appear in the Modularity'15 Proceedings in the ACM Digital Library. Submissions will be judged on the potential impact of the ideas and the quality of the presentation.

Program Committee Chair

Gary T. Leavens, University of Central Florida, USA (leavens@cs.ucf.edu)

Program Committee

Don Batory, University of Texas at Austin

Eric Bodden, Fraunhofer SIT and TU Darmstadt

Paulo Borba, Federal University of Pernambuco

Walter Cazzola, Università degli Studi di Milano

Cynthia Disenfeld, Technion -- Israel Institute of Technology

Robert Dyer, Bowling Green State University

Erik Ernst, Aarhus University

Matthew Flatt, University of Utah

Michael Haupt, Oracle Labs

Marieke Huisman, University of Twente

Cristina Lopes, University of California Irvine

Tiziana Margaria, University of Potsdam

Linda Northrop, Software Engineering Institute

Nate Nystrom, University of Lugano

Bruno C. d. S. Oliveira, The University of Hong Kong

Awais Rashid, Lancaster University

Henrique Rebêlo, Federal University of Pernambuco

Martin Rinard, Massachusetts Institute of Technology

Norbert Siegmund, University of Passau

Murali Sitaraman, Clemson University

Kevin Sullivan, University of Virginia

External Review Committee

Marsha Chechik, University of Toronto

Steven Edwards, Virginia Tech.

Dan Grossman, University of Washington

Görel Hedin, Lund University

Mira Mezini, TU Darmstadt

Peter Müller, ETH Zurich

Hridesh Rajan, Iowa State University

Clemens Szyperski, Microsoft Research

Éric Tanter, University of Chile

Eelco Visser, Delft University of Technology

For additional information, clarification, or answers to questions please contact the Program Committee Chair.

Locks

Locks allow restricting access to different areas of the code. A part of the code that we want only one thread to have access at a given time is called a critical section. This critical section can represent access to some resource (like a printer; we don't want another process to start printing in the middle), execution of a particular function or part within the program (like an ATM transaction, there should be no interference while it occurs), or a method of a distributed data type (avoid erasing while inserting an element to a list).

Let's see the following code (without locks)

public class Printer implements Runnable {

private String document;

public Printer(String document){
this.document = document;
}

@Override
public void run() {
Random r = new Random();
//represents some preprocessing of the document
try {
Thread.sleep(1000*(r.nextInt(2)+1));
} catch (InterruptedException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
for (int i=0; i < document.length(); i++){
System.out.println("printing \"" + document.charAt(i) + "\"");
try {
Thread.sleep(1000*(r.nextInt(2)+1));
} catch (InterruptedException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
}

public static void main(String[] args) {
Thread t1 = new Thread(new Printer("hello"));
Thread t2 = new Thread(new Printer("world"));
t1.start();
t2.start();
}

}

The main method starts two thread printing "hello" and "world" respectively. The run method of the Printer class (invoked when the threads are started), prints each letter and has some delay (imagine the physical time to actually print the letter. Then, when running this program the printing of both documents gets winded and the output letters do not form "hello" "world", but some mix of their letters.

One way to deal with this is by using locks within the for loop so that from the moment the printer starts it cannot get interrupted: (changes to the run method)

@Override

public void run() {

Random r = new Random();

//represents some preprocessing of the document

try {

Thread.sleep(1000*(r.nextInt(2)+1));

} catch (InterruptedException e1) {

// TODO Auto-generated catch block

e1.printStackTrace();

}

while (true){

boolean success = lock.tryLock();

if (success) break;

try {

Thread.sleep(1000*(r.nextInt(2)+1));

} catch (InterruptedException e) {

// TODO Auto-generated catch block

e.printStackTrace();

}

}

for (int i=0; i < document.length(); i++){

System.out.println("printing \"" + document.charAt(i) + "\"");

try {

Thread.sleep(1000*(r.nextInt(2)+1));

} catch (InterruptedException e) {

// TODO Auto-generated catch block

e.printStackTrace();

}

}

lock.unlock();

}

Now, only one thread can access the for loop at a time. 

Question to think: what would have happened had we forgotten the unlock after the loop?

PS: The goal of this post was to give a first explanation of locks (without entering into language details) Java allows using synchronized for avoiding multiple threads from entering the same method. For a discussion on the difference between locks and synchronize, there's a nice explanation here: locks vs synchronized

LOTOS

LOTOS (Language of Temporal Ordering Specifications) is a formal specification language that allows expressing processes and process compositions.

There is a wide set of operators with which very interesting behaviors and process interactions can be obtained. But first, we'll start from the basics.

The basic process is an event, and an event is a communication through a gate, for instance, receiving through a gate g an integer value x

g?x:int

or providing as output "hello" through the gate h

h!"hello"

Notice that we represent input with a question mark and output with an exclamation mark. In addition, when g receives the value within x, the variable x is locally accessible to the following events.. but now we ask ourselves, how to add events?

The simplest case is the sequential composition, obtained with the semicolon (;)

for instance

g?x:int; g!x

this process receives an int value, and then outputs it through the same gate

Different gates and variables could be involved. For instance

g?x:int; g?y: string; h!concat(y, " world"); f!x+2

In the next LOTOS post I will discuss choice (choosing between enabled behaviors)

A Lotus flower

Aspect-oriented Programming (AOP) - around advice

We have discussed before and after advice (After, AOP - 2), it remains to talk about around advice. This kind of advice is very interesting because not only allows adding behavior before and/or after the original joinpoint, but also allows overriding the original behavior, or applying the original behavior multiple times.

For example,

public class C{

  public static void main(){
1    int y = addOne(0);
2    System.out.println(y);
  }

  public static int addOne(int x){
3    return x+1;
  }
}

public aspect A{
4  pointcut callAddOne(int x): call(* *.addOne(int)) && args(x)

5  int around(int x): callAddOne(x){
6    System.out.println("before calling");
7    int tmpValue = proceed(x);
8    tmpValue = proceed(tmpValue);
9    System.out.println("after calling");
10    return tmpValue;
  }
}

In the example, the around advice (line 5) is activated when the pointcut (line 4) matches a joinpoint. The only location in C where this occurs is in line 1, when addOne is called.
Then, the following things happen
i) when matching the joinpoint, the pointcut caputres x as the argument to the call (notices args(x) within the pointcut definition)
ii) the message "before calling" is printed
iii) proceed indicates to apply the original behavior. That is, we are actually calling to addOne with the value x (in the original call was 0, so this is the value within the advice).
iv) tmpValue obtains the return value of the call, in this case 1
v) we call again to the original method! but this time with the argument tmpValue
vi) tmpValue is updated to 2 (it was incremented by the second proceed)
vii) the second message within the advice is printed
viii) the value 2 is returned
ix) y (in line 1) receives 2 and gets printed.


Around-like advice are a very strong mechanism not only to add behavior before or after the original, but also to change the control flow, for instance by making the original joinpoint to be executed multiple times, or none at all! If within the around advice there is no proceed, then the original behavior gets overriden.

The Earth moves around the Sun (but doesn't override it :) )

Pre and Post Conditions: Hoare Logic - 2

Continuing the post Hoare Logic - 1, we will now present to which kind of statements these triples (pre, program, post) can be applied
0. Nop (doesn't do anything)
1. Assignments
x := e // x gets the value of some expression e, that may or may not contain x
2. Consequence; that is, S1;S2 (first execute S1, then S2)
3. if B then S1 else S2 fi (typical if, with B a boolean condition)
4. while B do S od (at each iteration, B is checked. If satisfied by the current state, S is executed)

All these statements can then be combined to make more complex programs, and provide the formalization to prove program correctness

For example, given P:

y := 2*x;
if (y < 0) z := - y/2
else z := y/2
fi

we can prove that the value of z is the absolute value of x (the division is the real division, not the integer one).

To do so we can instrument the program above as follows:

1. {\(x=X_0\)}
y := 2*x;
2. {\(x=X_0 \land y = 2\cdot x\)}
if (y < 0)
  z := - y/2
3.  {\(x=X_0 \land y = 2\cdot x \land z = - y/2\)}
else
   z := y/2
4.  {\(x=X_0 \land y = 2\cdot x \land z = y/2\)}
fi

5. {\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)  \land (y\ge 0 \rightarrow z = y/2)\)}

Line 1 adds an auxiliary variable (X₀) - which doesn't appear in the program - to indicate that the contents of x do not change. Auxiliary variables can be added at any stage of the proof, but their value does not change; that is, from the moment we have indicated x = X₀ in 1, we have indicated that X0 will always contain x's initial value

Line 2 adds the assignment to y, and that x has not changed

Line 3 considers the first branch of the if, and Line 4 the second branch, updating z as necessary

Line 5 joins both branches, according to the condition. That is, if y <0 then the first branch is applied, otherwise the second one.

5. {\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)  \land (y\ge 0 \rightarrow z = y/2)\)}
Now given this last expression, we'll try to conclude that indeed z contains the absolute value of x

From
\(x=X_0 \land y = 2\cdot x \land (y<0 \rightarrow z = - y/2)\)
It can be inferred that when y<0 the value of z is -X₀
Similarly, from the second implication it can be inferred that when y is greater or equal than 0, the value of z is X₀.

Now, y is lower than 0 iff x is lower than 0, therefore,
the value of z is -X₀ if x is lower than 0, and X₀ otherwise, which is the definition of the absolute value, as expected.

Aspect-oriented Programming (AOP) - AJDT - First project

To actually define pointcuts (Pointcuts - 1, Pointcuts - 2), advice (Introduction - 2, after advice), and aspects in general, AJDT is a useful tool. According to your eclipse version, download instructions are available in AJDT - download.

That is, you open eclipse, go to Help -> Install new Software ; enter the appropriate update site, and install AJDT.

Once installed, you can define an AspectJ project, with classes and aspects.

Creating an AspectJ project:

In the next window, set the project name.

A project that has not initially been set as an AspectJ project, can later be changed (and an AspectJ project can be changed to a normal java project - but if it has aspects, it will fail to compile)

Add a new class HelloWorldAspectsMain

with the following methods:

public static void main(String[] args) {
foo();
}

private static void foo() {
           System.out.println("in foo"); 
}

Then, create the aspect HelloWorldAspect (new -> Other.. -> Aspect) 

The contents of the created file are:

public aspect HelloWorldAspect {

}

Within the brackets add the following code:

pointcut callFoo(): call(* *.foo());

before(): callFoo(){

System.out.println("Hello");

}

after(): callFoo(){

System.out.println("World!");

}

so that the resulting aspect file is:

public aspect HelloWorldAspect {

pointcut callFoo(): call(* *.foo());

before(): callFoo(){

System.out.println("Hello");

}

after(): callFoo(){

System.out.println("World!");

}

}

Run the code as an AspectJ program (when pressing run, this option should appear), and check what happens!

The expected output is:

Hello

in foo

World!