M*: Multidisciplinar Multiobjective Metaheuristics

| TIN2008-06491-C04-01 Ministerio de Ciencia e Innovación (Spain)
| UMA - University of Málaga



list 26th Oct 2011. Incoming, coordination meeting, UMA (Málaga) [AGENDA]

list 11th Mar 2011. Incoming, coordination meeting, UC3M (Leganés) [AGENDA]

list [Engineering Optimization] Special issue on Multiobjective Metaheuristics for Multidisciplinary Engineering Applications

list 16th Jul 2010. Incoming, coordination meeting, UEX (Cáceres)

list [META'10] Special Session on Real Parameter Optimization: From Benchmarking To Real World Applications

list 5th Feb 2010. Coordination meeting, ULL (La Laguna)

list 14th Dec 2009. Coordination meeting, UMA (Málaga)

list 3rd Jul 2009. First Problem's Workshop, UMA (Málaga)

list 17th April 2009. Problem descriptions, instances, codes ... [+]

list 2nd April 2009. M* Web Site Launched




Model Checking


Model checking [2] is a fully automatic technique that allows to check if a given concurrent system satisfies a property like, for example, the absence of deadlocks, the absence of starvation, the fulfilment of an invariant, etc. The use of this technique is a must when developing software that controls critical systems, such as an airplane or a spacecraft. However, the memory required for the verification usually grows in an exponential way with the size of the system to verify (state explosion problem).

When the search for errors with a low amount of computational resources (memory and time) is a priority (e.g., in the first stages of the development), non-exhaustive algorithms using heuristic information can be used. In this case metaheuristic algorithms can be applied to find short error trails of software models.

Model Checking


The problem of finding errors in software models can be translated into the search of a path in a graph (the Büchi automaton) starting in the initial state and ending in an objective node (accepting state) and an additional cycle involving the objective node. We can formalize the problem as follows.

Let G=(S,T) be a directed graph where S is the set of nodes and T is the set of arcs. Let q be the initial node of the graph and F a set of distinguished nodes that we call final nodes. We denote with T(s) the successors of node s. A finite path over the graph is a sequence of nodes π = s1 s2 ... snwhere si are states and si belongs to T(si-1) for i=2,...,n. We denote with πi the i-th node of the sequence and we use |π| to refer to the length of the path, that is, the number of nodes of π. We say that a path π is a starting path if the first node of the path is the initial node of the graph, that is, π1=q. We will use π* to refer to the last node of the sequence π, that is, π* = π|π|. We say that a path π is a cycle if the first and the last nodes of the path are the same, that is, π1=π*.

Given a directed graph G, the problem at hand consists in finding a starting path π ending in an final node plus a cycle ν containing the final node. That is, find π and ν subject to π1 = q, π* belongs to F and π*=ν1=ν*.

The graph G used in the problem is derived from the Büchi automaton B (synchronous product of the concurrent system and the never claim in Spin). The set of nodes S in G is the set of states in B, the set of arcs T in G is the set of transitions in B, the initial node q in G is the initial state in B, and the set of final nodes F in G is the set of accepting states in B. For more details see [1,3].


Promela models

With the Spin and HSF-Spin source code a lot of Promela models can be found. In addition, there exists a benchamark with more than 300 software models (BEEM). The Spin source code can be downloaded from here and the HSF-Spin source code from here. The BEEM benchmark can be found here.


Related Bibliography and Papers

[1] F. Chicano and E. Alba, Ant Colony Optimization with Partial Order Reduction for Discovering Safety Property Violations in Concurrent Models, Information Processing Letters, 106 (6): 221-231

[2] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000

[3] F. Chicano, E. Alba, Searching for Liveness Property Violations in Concurrent Systems with ACO, Genetic and Evolutionary Computation Conference, pp. 1727-1734, Atlanta, USA

Last Updated: 14/12/09
For any question or suggestion, click here to contact with us.
joomla counter | Webmaster | Contact Us | ©2009 M* UMA