hosted by
publicationslist.org
    

Steve Hostettler

Steve Hostettler

Université de Genève
CUI - Battelle bat. A
Route de Drize, 7
CH-1227 Carouge

Tél. : +41 22 379 01 60
Fax : +41 22 379 0250
steve.hostettler@unige.ch

Journal articles

2012
Steve Hostettler, Alexis Marechal, Alban Linard, Matteo Risoldi, Didier Buchs (2012)  High-Level Petri Net Model Checking with AlPiNA   Fundamenta Informaticae 113: 3-4. 229-264 Feb  
Abstract: Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri nets. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.
Notes:
2011
2006

Conference papers

2011
2010
2009
Didier Buchs, Steve Hostettler (2009)  Sigma Decision Diagrams   In: TERMGRAPH 2009 : Premiliminary proceedings of the 5th International Workshop on Computing with Terms and Graphs Edited by:Andrea Corradini. 18-32 Università di Pisa  
Abstract: Encoding and rewriting of large set of terms is very useful in a number of domains, such as model checking and theorem proving. The challenge of encoding and normalizing several billions of terms requires efficient ways of representing and manipulating them. Term Graph Rewriting is a well-known technique to share common sub-terms and thus to save both memory and processing time. However, this does not always t well to the operational framework since it destroys the original structure and replaces it by a new one. This paper introduces a new kind of Decision Diagrams (DD), especially designed to handle set of terms in an efficient way. Based on the Set Decision Diagrams(SDD), an evolution of the well-known Binary Decision Diagrams(BDD), we propose the Sigma Decision Diagrams (Sigma DD), a new approach to perform Term Rewriting on a set of terms in order to compute the image of that set effciently.
Notes:

Technical reports

2009
Didier Buchs, Steve Hostettler (2009)  Toward efficient state space generation of algebraic Petri nets.   Université de Genève, Centre Universitaire d’Informatique SMV technical report series 206. Battelle Bat. A Route de Drize 7 1227 Carouge Switzerland:  
Abstract: Algebraic Petri Nets (APN: Petri Nets + Abstract Algebraic Data Types) are powerful tools to model concurrent systems. Because of their high expressive power, allowing end-user to model more complex systems, State Space Explo- sion is a big issue in APN. Symbolic Model Checking (SMC) and particularly Decision Diagrams (DD) based symbolic model checking is a proven technique to handle the State Space Explosion for simpler formalisms such as P/T Petri Nets. This paper discusses how to use Binary Decision Diagramsâ (BDD) evo- lutions (Data Decision Diagrams, Set Decision Diagrams, Σ DD, . . . ) to tackle aforementioned problem in the APN world. The main contributions of this work are the encoding of any APN model using the DD framework and the notion of Algebraic Cluster that tackles the concurrency induced by the token multiplic- ity. The discussed algorithms have been implemented in a tool that is freely accessible on http://alpina.unige.ch.
Notes:
2008
Steve Hostettler (2008)  Java Decisions Diagrams Library   Université de Genève, Centre Universitaire d’Informatique SMV technical report series 201. Battelle Bat. A Route de Drize 7 1227 Carouge Switzerland:  
Abstract: This paper presents the Java Decisions Diagrams Library, which is a framework to easily build and use Data and Set Decisions Diagrams on the Java platform.
Notes:

Tutorials

2006
Steve Hostettler (2006)  Spring : théorie & pratique   Online [Tutorials]  
Abstract: Cet article traite du framework Spring. A la fois de sa mise en oeuvre et de certains des concepts théoriques sur lesquels il repose. Comme par exemple l'injection de dépendance ou encore la programmation orientée aspect.
Notes:
Steve Hostettler (2006)  Couplage Apache HTTP & Tomcat   Online [Tutorials]  
Abstract: Cet article explique comment intégrer le moteur de servlet Apache-Tomcat et le serveur Apache-HTTP, afin de sécuriser (HTTPS) une application Inter/intranet, de faciliter l'accès à cette application par l'utilisation de noms simplifiés (Rewriting) et enfin permettre une tolérance aux pannes (failover) et une répartition de charge (load-balancing).
Notes:

PhD theses

2011
Steve Hostettler (2011)  High-Level Petri Net Model Checking   Université de Genève, Faculté des sciences, département d'informatique  
Abstract: Although model checking is heavily used in the hardware domain, its use is not mainstream in software engineering yet. Modeling of software system is tedious using low-level formalisms such as Place/Transition Petri Nets. Moreover, usual verification techniques (e.g., state space analysis) are often intractable because of the infamous State Space Explosion. While modeling can be eased by using high-level formalisms such as High- level Petri Nets that make models more concise and more readable, State Space Explosion is still an important challenge. Many authors have tackled this issue on High-level Petri Nets, mostly by either modularizing the system or by reducing the states to consider (e.g., partial orders, symmetries). Most of those approaches encode the state space explicitly, i.e., the required amount of memory is linear to the number of states, which is rapidly intractable due to State Space Explosion. Symbolic Model Checking partially overcomes this problem by encoding the state space in a condensed way using Decision Diagrams and has been successfully applied to Place/Transition Petri Nets. Albeit very effective, to be applied to High-level Petri Nets, these techniques require to âunfoldâ the High-level Petri Nets to an equivalent Petri nets. This is sometimes impractical because it might be difficult, if not infeasible, to figure out the data types boundaries. To partially overcome these problems, we propose to apply Symbolic Model Checking at the High-level Petri Net level directly. To that end, we propose the Σ Decision Diagrams a kind of Decision Diagrams especially created to handle large sets of terms representing the instances of the data types. Besides, we introduce the notion of Partial Net Unfolding that avoids having to unfold all data types prior model checking. Moreover, we describe Algebraic Clustering that adapts the concept of clustering to High-level Petri Nets and therefore that allows to apply advanced techniques such as saturation. These contributions pave the way to the application of Symbolic Model Checking to modular extensions of the High-level Petri Net. Finally, as a proof of concept, we implemented all the proposed techniques in a model checker called the Algebraic Petri Nets Analyzer.
Notes:
Powered by PublicationsList.org.