Franck Pommereau

SNAKES 0.9.16 released

2011-06-07T16:56:00.000+02:00

This release introduces a first version of a graphical ABCD simulator. Invoking command abcd with option --simul yields a window in which you may execute your ABCD code interactively, going back and forth into the trace executed so far. The top-right panel shows the source code, with the currently executable actions highlighted. The top-left panel shows all the currently executable actions with

SNAKES 0.9.15 released

2011-05-10T21:24:00.001+02:00

This new version successfully passes the tests under Python 3.2, only the doctests have been passed, so there is probably still undetected compatibility problems. Notice that tests fail on Python 3.1, but presumably everybody already has 3.2 considering how long 3.1 has existed. Other changes in this release include small bug fixes and a new ABCD example (dinning philosophers). So far, SNAKES is

SNAKES roadmap

2011-04-18T20:24:00.001+02:00

I've been asked a few times how SNAKES version are numbered. As for many software, it is major.minor.revision. But I currently stick with major=0 and reached minor=9 already, so I'm currently only incrementing the revision number. Before to move to major=1, I'll wait to have the following changes implemented: PNML support replaced: a Python implementation of the PNML standard is in progress, it

SNAKES 0.9.14 released

2011-04-18T20:02:00.000+02:00

This new version features a complete rewrite of the ABCD compiler. The main visible changes are: internal error on syntax errors should be gone! :-) a few new keywords (task, enum, typedef, const, symbol) enumerated types formerly declared as in(value, ...) should be rewritten as enum(value, ...) new types can be declared using typedef name = type and reused in a buffer declaration

New home page at IBISC

2010-11-22T14:07:00.000+01:00

My home page at LACL does not exist any more: I've moved to IBISC as a professor and built a new home page there. I've migrated most of the old content except: publications that have been hosted since a few months on this blog; outdated pages; SNAKES API reference manual since it is distributed together with SNAKES. I also plan to host a copy of SNAKES API on SNAKES development page (as soon as

Algebras of coloured Petri nets

2010-10-07T12:47:00.000+02:00

Franck Pommereau LAP LAMBERT Academic Publishing October 2010, ISBN: 978-3-8433-6113-2 Available for purchase here Blurp. This book surveys more than ten years of research work about a framework of composable coloured Petri nets. This framework is organised around a core model of coloured Petri nets that can be extended with various features: control flow, synchronous communication,

Qualitative modelling and analysis of regulations in multi-cellular systems using Petri nets and topological collections

2010-08-27T11:29:00.002+02:00

Jean-Louis Giavitto, Hanna Klaudel and Franck Pommereau Proc. of MeCBIC'10, EPTCS vol.40, 2010 Abstract. In this paper, we aim at modelling and analyzing the regulation processes in multi-cellular biological systems, in particular tissues. The modelling framework is based on interconnected logical regulatory networks (à la René Thomas) equipped with information about their spatial

SNAKES moves to Google code

2010-08-19T16:07:00.000+02:00

I decided to move SNAKES from Launchpad to Google code. The main reasons for this change are: ease of use: Launchpad has always been for me a nightmare to use. In contrast, I immediately felt comfortable with Google code speed: Google code is much, much faster features: Google code provides a wiki, I can track visits and downloads I'll keep using Launchpad to host SNAKES' Ubuntu packages, for

SNAKES 0.9.13 released

2010-07-16T17:46:00.002+02:00

Update: by mistake, the released source tarball did contain version 0.9.12; this has been fixed. You may need to download it again if you've installed from source before July 21th. This release introduces inhibitor arcs (see below) as well as a layout methods for Petri nets with plugin gv: added inhibitor arcs added Ubuntu Lucid (10.04) package fixed data.WordSet.fresh when base is used fixed

Modelling, Verification, and Formal Analysis of Security Properties in a P2P System

2010-05-19T12:07:00.002+02:00

Sam Sanjabi and Franck Pommereau Proc. of COLSEC'10, IEEE Digital library, IEEE, 2010 Abstract. We present a security analysis of the SPREADS system, a distributed storage service based on a centralized peer-to-peer architecture. We formally modelled the salient behavior of the actual system using ABCD, a high level specification language with a coloured Petri net semantics, which allowed the

SNAKES 0.9.12 released

2010-04-01T20:22:00.002+02:00

This release is now compatible with CPython (2.5 and 2.6), PyPy (1.2), Unladen-Swallow (2.6.1) and Jython (2.5.1). PyGraphviz is no more required, which improves the portability to Windows and MacOS X: SNAKES should now work out of the box if GraphViz is properly installed. Various bugs have been fixed: fixed snakes.plugins.clusters.rename_node fixed snakes.nets.Flush.flow fixed an uncaught

SNAKES 0.9.11 released

2010-03-25T20:23:00.002+01:00

Various bugs have been fixed: failing doctests issues with attributes locking missing __hash__ methods nodes renamed to themselves in ABCD Minor features have been added: snakes.nets.Evaluator.__contains__ base argument to snakes.data.WordSet option --symbols to ABCD compiler and snakes.data.Symbol naming of net instances in ABCD (new syntax name::Foo()) logo let function to update bindings

Using SNAKES plugins

2010-01-18T17:20:00.002+01:00

One of the important features of SNAKES is its capability to extend the basic model with plugins. In this post, we see how to load plugins. Loading a plugin essentially requires a call to snakes.plugins.load. For instance, let's load plugin gv that allows to draw Petri nets (using GraphViz): import snakes.plugins snakes.plugins.load("gv", "snakes.nets", "mynets") This call to load can be

Arc annotations in SNAKES

2010-01-18T16:13:00.001+01:00

Most arcs in a Petri net within SNAKES are annotated with values, expressions or variables. However, other types of annotations are available. This post reviews all the types of arc annotations available in SNAKES. To illustrate the various arc annotations, we will use a simple net pattern generated with the following factory function that creates a net one transition to consume cons from an

Getting SNAKES and installing it

2010-01-17T13:14:00.001+01:00

A package for Ubuntu Linux is available at my LaunchPad PPA. Instructions are provided there to tell your package manager about where to find SNAKES. The package itself is called python-snakes, it declares the appropriate dependencies so that SNAKES can be used right after installation. To install from source, first download the latest version from SNAKES download page. Then uncompress the

The SNAKES toolkit

2010-01-17T11:54:00.004+01:00

SNAKES is a Python library that provides all then necessary to define and execute many sorts of Petri nets, in particular those of the PBC and M-nets family. Its main aim is to be a general Petri net library, being able to cope with most Petri nets models, and providing the researcher with a tool to quickly prototype its new ideas. SNAKES should be suitable to provide the data model for editors

Firing rule in SNAKES

2010-01-16T15:13:00.004+01:00

In SNAKES, one cannot use Expression objects as input arcs annotations, moreover, all the variables used in a transition guard and output arcs should be bound through (at least) one of the input arcs. These restrictions can be explained. When calling method t.modes(), the available modes are computed by matching the input arcs annotations with respect to the available tokens in the corresponding

First steps with SNAKES

2010-01-15T17:26:00.009+01:00

In this post, we define a simple coloured Petri net and see how to fire transitions and get markings. Let's consider a simple coloured Petri net with a single transition that increments an integer valued token (so, 0 is the value of the token, not a number of tokens) token held by a single place, the incrementation stops when the value is 5 thanks to a guard on the transition. To define this net

PGP public key

2010-01-14T21:06:00.002+01:00

This is my PGP/GPG public key: -----BEGIN PGP PUBLIC KEY BLOCK----- Version: GnuPG v1.4.9 (GNU/Linux) mQGiBDoc8C4RBACwNvvDf+a9yuMLHK1xB/QX6pcHxvzhfTXVEZZYzQtrvjsgE3PP wEFrtfg/5/klu+AJIxxevCd1V0tptLDvfEGaYacyAumFQGfWc6Yv3VfziTdhpjyt Zd5GnT8lSLhB4ZfMYuze+6Mc2F3KBIsS10r5R8hvSjNFg7vdvWCk82v75wCghzyk aae77hUugdP3F101xSOhmi8D/jgDJX9iGvHejd9Altx3kc2/mE8doQfAahM4ZeSo

Algebras of coloured Petri nets

2010-01-14T18:45:00.003+01:00

Franck Pommereau Habilitation thesis, university Paris-East, 2009. Abstract. This document surveys my research work about a framework of composable coloured Petri nets. This framework is organised around a core model of coloured Petri nets that can be extended with various features: control flow, synchronous communication, exceptions, threads, functions and time. Extensions are made in such a

Nets in nets with SNAKES

2010-01-14T18:38:00.002+01:00

Franck Pommereau Proc. of MOCA'09, M. Duvigneau and D. Moldt editors, Universität Hamburg, Dept. Informatik, 2009 Abstract. This paper presents the toolkit SNAKES, focusing on the ability to model Petri nets whose tokens are Petri nets (so called nets in nets). SNAKES is a general Petri net library that allows to model and execute Python-coloured Petri nets: tokens are Python objects and net

An Approach to State Space Reduction for Systems with Dynamic Process Creation

2010-01-14T18:36:00.002+01:00

Hanna Klaudel, Maciej Koutny, Elisabeth Pelz and Franck Pommereau Proc. of ISCIS'09, IEEE digital library 15777, IEEE, 2009 Abstract. Automated verification of dynamic multi-threaded computing systems can be adversely affected by problems relating to dynamic process creation. We therefore investigate—in a general setting of labelled transition systems—a way of reducing the state spaces of

Quickly prototyping Petri nets tools with SNAKES

2010-01-14T18:32:00.003+01:00

Franck Pommereau Proc. of PNTAP'08, ACM Digital Library, ACM, 2008 Abstract. This paper presents the toolkit SNAKES that is aimed at providing a flexible solution to the problem of quickly prototyping Petri nets tools. In particular, SNAKES is expected to have as few built-in limitations as possible with respect to the particular variant of Petri net to be used. The goal is to make SNAKES

Quickly prototyping Petri nets tools with SNAKES

2010-01-14T18:28:00.002+01:00

Franck Pommereau Petri net newsletter, October 2008 Abstract. This paper presents the toolkit SNAKES that is aimed at providing a flexible solution to the problem of quickly prototyping Petri nets tools. In particular, SNAKES is expected to have as few built-in limitations as possible with respect to the particular variant of Petri net to be used. The goal is to make SNAKES suitable for any kind

Towards Efficient Verification of Systems with Dynamic Process Creation

2010-01-14T18:26:00.002+01:00

Hanna Klaudel, Maciej Koutny, Elisabeth Pelz and Franck Pommereau Technical report, LACL, 2008 Abstract. Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic

Towards Efficient Verification of Systems with Dynamic Process Creation

2010-01-14T18:24:00.002+01:00

Hanna Klaudel, Maciej Koutny, Elisabeth Pelz and Franck Pommereau Proc. of ICTAC'08, LNCS 5160, Springer, 2008 Abstract. Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to propose a technical device for coping with one such obstacle, namely that caused

Modeling and analysis of security protocols using role based specifications and Petri nets

2010-01-14T18:21:00.002+01:00

Roland Bouroulet, Raymond Devillers, Hanna Klaudel, Elisabeth Pelz and Franck Pommereau Proc. of ICATPN'08, LNCS 5062, Springer, 2008 Abstract. In this paper, we introduce a framework composed of a syntax and its compositional Petri net semantics, for the specification and verification of properties (like authentication) of security protocols. The protocol agents (e.g., an initiator, a responder

M-nets: a survey

2010-01-14T18:19:00.002+01:00

Hanna Klaudel and Franck Pommereau Acta Informatica 45(7-8), Springer, 2008 Abstract. This paper surveys the research related to the model of M-nets since it was introduced in 1995. M-nets are high-level labelled Petri nets which can be composed, like process algebra terms, using various operators. We present the core model, several of its extensions and the main applications. Keywords.

Efficient reachability graph representation of Petri nets with unbounded counters

2010-01-14T18:17:00.003+01:00

Franck Pommereau, Raymond Devillers and Hanna Klaudel Proc. of Infinity'07, ENTCS, Elsevier, 2007 Abstract. In this paper, we define a class of Petri nets, called Petri nets with counters, that can be seen as place/transition Petri nets enriched with a vector of integer variables on which linear operations may be applied. Their semantics usually leads to huge or infinite reachability graphs.

Versatile Boxes: a Multi-Purpose Algebra of High-Level Petri nets

2010-01-14T18:11:00.002+01:00

Franck Pommereau Proc. of DADS/SCSC'07, SCS/ACM, 2007 Abstract. This paper introduces a model of composable Petri nets, called Versatile Boxes, that has all the high-level features already introduced in the family of the Petri Box Calculus (mainly: data and time representation) as well as a new interruption capability. This allows for defining processes that are able to interrupt their execution

Petri nets as Executable Specifications of High-Level Timed Parallel Systems

2010-01-14T18:08:00.002+01:00

Franck Pommereau SCPE/PDPC 6.4, pages 71-82, SWPS, 2005 Abstract. We propose to use high-level Petri nets as a model for the semantics of high-level parallel systems. This model is known to be useful for the purpose of verification and we show that it is also executable in a parallel way. Executing a Petri net is not difficult in general but more complicated in a timed context, which makes

Petri nets as Executable Specifications of High-Level Timed Parallel Systems

2010-01-14T18:00:00.003+01:00

Franck Pommereau Proc. of PAPP/ICCS'04, LNCS 3038, Springer, 2004 Abstract. We propose to use high-level Petri nets for the semantics of high-level parallel systems. This model is known to be useful for the of verification and we show that it is also executable in a parallel way. Executing a Petri net is easy in general but more complicated in a timed context, which makes necessary to

Box Calculus with High-Level Buffers

2010-01-14T17:58:00.002+01:00

Cécile Bui Thanh, Hanna Klaudel and Franck Pommereau Proc. of DADS/ASTC'04, SCS, 2004 Abstract. In this paper, we propose a high-level process algebra allowing to express the exchange of data values using both handshake and buffered communication. This allows a simple and compositional expression of interprocess communication; in particular the buffered one makes easy the representation of

Causal Time Calculus

2010-01-14T17:55:00.003+01:00

Franck Pommereau Proc. of FORMATS'03, LNCS 2791, Springer, 2004 Abstract. We present a process algebra suitable to the modelling of timed concurrent systems and to their efficient verification through model checking. The algebra is provided with two consistent semantics: a structural operational semantics (as usual for process algebras) and a denotational semantics in terms of Petri nets in

Asynchonous Box Calculus

2010-01-14T17:52:00.002+01:00

Raymond Devillers, Hanna Klaudel, Maciej Koutny and Franck Pommereau Fundamenta Informaticae, 54(1), IOS Press, 2003 Abstract. The starting point of this paper is an algebraic Petri net framework allowing one to express net compositions, such as iteration and parallel composition, as well as transition synchronisation and restriction. We enrich the original model by introducing new constructs

Modèles composables et concurrents pour le temps-réel

2010-01-14T17:46:00.002+01:00

Franck Pommereau PhD Thesis, Université Paris 12, 2002 Note. This thesis is written in French Abstract. This thesis is concerned with the modelling of real-time systems using Petri nets. We investigate both the problem of time representation, and of preemption (i.e., interruption of the processes of a system) which is often needed for real-time applications. We consider Petri nets without

Petri nets with causal time for system verification

2010-01-14T16:34:00.002+01:00

Cécile Bui Thanh, Hanna Klaudel and Franck Pommereau Proc. of MTCS'02, ENTCS 68(5), Elsevier, 2003 Abstract. We present a new approach to the modelling of time constrained systems. It is based on untimed high-level Petri nets using the concept of causal time. With this concept, the progression of time is modelled in the system by the occurrence of a distinguished event, tick, which serves as a

Operational Semantics for PBC with Asynchronous Communication

2010-01-14T16:31:00.002+01:00

Raymond Devillers, Hanna Klaudel, Maciej Koutny, Elisabeth Pelz and Franck Pommereau Proc. of HPC'02, SCS, 2002 Abstract. This paper presents two related algebras which can be used to specify and analyse concurrent systems with synchronous and asynchronous communications. The first algebra is based on a class of P/T-nets, called boxes, and their standard transition firing rule. It is an

A class of composable and preemptible high-level Petri nets with an application to multi-tasking systems

2010-01-14T16:28:00.002+01:00

Hanna Klaudel and Franck Pommereau Fundamenta Informaticae, 50(1), IOS Press, 2002 Abstract. This paper presents an extension of an algebra of high-level Petri nets with operations for suspension and abortion. These operations are sound with respect to the semantics of preemption, and can be applied to the modelling of the semantics of high-level parallel programming languages with

Box Calculus with Coloured Buffers

2010-01-14T16:23:00.002+01:00

Cécile Bui Thanh, Hanna Klaudel and Franck Pommereau Technical report 2002-16, LACL, 2002 Abstract. The starting point of this paper is the asynchronous box calculus with multi-way communication (MBC), a formalism suitable for modelling compositionally distributed systems using both synchronous and asynchronous communication and a number of control flow operators. MBC is composed of two

An Algebra of Non-safe Petri Boxes

2010-01-14T16:19:00.001+01:00

Raymond Devillers, Hanna Klaudel, Maciej Koutny and Franck Pommereau Proc. of AMAST'02, LNCS 0302. Springer, 2002. Abstract. We define an algebraic framework based on non-safe Petri nets, which allows one to express operations such as iteration, parallel composition, and transition synchronisation. This leads to an algebra of process expressions, whose constants and operators directly

A concurrent semantics of static exceptions in a parallel programming language

2010-01-14T16:15:00.001+01:00

Hanna Klaudel and Franck Pommereau Proc. of ICATPN'01, LNCS 2075, pages 204-223, Springer, 2001 Abstract. This paper aims at introducing a mechanism of exceptions in a parallel programming language, giving them a formal concurrent semantics in terms of preemptible and composable high-level Petri nets. We show that, combined with concurrency, exceptions can be used as a basis for other

A concurrent and compositional Petri net semantics of preemption

2010-01-14T16:07:00.003+01:00

Hanna Klaudel and Franck Pommereau Proc. of IFM'00, LNCS 1945, pages 318-337, Springer, 2000 Abstract. The aim of this paper is the introduction of preemption in a compositional model, called M-nets, which is based on Petri nets and hence provided with a concurrent semantics. We propose a way to model preemptible systems by extending the M-net model with priorities and the M-net algebra with a

FIFO buffers in tie sauce

2010-01-14T15:42:00.001+01:00

Fanck Pommereau Proc. of DAPSYS'00, pages 95-104, Kluwer Academic Publishers, 2000 Abstract. This paper introduces a new semantics for FIFO buffers (more usually called channels) in a parallel programming language, B(PN)². This semantics is given in terms of M-nets, which form an algebra of labelled high-level Petri nets. The proposed approach makes usage of asynchronous link operator, newly

FIFO buffers is hot tie sauce

2010-01-14T15:38:00.002+01:00

Franck Pommereau and Christian Stehno Technical report 2001-04, LACL, 2001 Abstract. This paper introduces a new semantics for FIFO buffers (usually called channels) in a parallel programming language, B(PN)². This semantics is given in terms of M-nets, which form an algebra of labelled high-level Petri nets. The proposed approach uses the asynchronous link operator, newly introduced in the

Asynchronous links in the PBC and M-nets

2010-01-14T15:30:00.005+01:00

Hanna Klaudel and Franck Pommereau Proc. of ASIAN'99, LNCS 1742, pages 190-200, Springer, 1999 Abstract. This paper aims at introducing an extension of M-nets, a fully compositional class of high-level Petri nets, and of its low-level counter part, Petri Boxes Calculus (PBC). We introduce a new operator with nice algebraic properties which allows to express asynchronous communications in a

Integrating Beamer with Impressive

2009-11-27T15:43:00.006+01:00

I recently adopted Beamer to prepare slide-shows using LaTeX. It really has a lot of features that make you life easier. In particular the \uncover command changed my life when it came to prepare animations. Then I decided to adopt Impressive to display the presentation. Compared with other PDF viewers, it has two features that I really appreciate: the overview page and the timer (to measure time

Copying local mail to Gmail

2009-07-17T17:46:00.004+02:00

Here is a simple script that reads a mailbox and transfer its content to a Gmail account. Other solutions I've found are SMTP-based which causes modifications of the transferred emails. But, using IMAP, it is possible to copy email to a remote mailbox. (Of course, this can be done graphically using an email client that supports IMAP, see this post for instructions.) This script can be customised

Interfacing Java and Python through JNI and Cython

2009-05-19T15:59:00.003+02:00

This post shows how to invoke Python code from a Java program. Various tools exist for this purpose (see this survey on communications between Java and Python), in particular there is Jepp that is perfect when what you need is to call Python scripts from Java or just fetch some values from a Python interpreter. But when you need a lower level communication, eg, call a Python function from Java

From string formatting to parsing

2009-05-12T21:19:00.013+02:00

With Python's string formatting operator, you can do: >>> format = "I'd like to eat %u %s of spam with %u eggs" >>> data = (3, "pounds", 10) >>> text = format % data >>> text "I'd like to eat 3 pounds of spam with 10 eggs" But how to perform the reverse operation: given text and format, how to get data? The idea is to analyse format and replace each % directive with the corresponding regexp.

Copy a Python dict with updates

2009-05-12T18:41:00.006+02:00

For my first post: a small trick I've recently discovered.Suppose you have a dict that you want to copy while changing the values of some keys. A single instruction can do it:new = dict(old, a=1, b=2, c=3) This is equivalent to:new = old.copy() new.update({"a": 1, "b": 2, "c": 3})