24documents trouvés
A timed graphical interval logic
N.ABID, S.DAL ZILIO
VERTICS
Rapport LAAS N°12368, Juillet 2012, 4p.
Diffusable
127688Model-checking support for AADL
S.DAL ZILIO, F.VERNADAT, B.BERTHOMIEU, M.FILALI, J.P.BODEVEIX
VERTICS, IRIT-UPS
Rapport LAAS N°12758,
Diffusable
129022Parallel model cheking with lazy cycle detection MCLCD
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
VERTICS
Rapport LAAS N°12139, Mars 2012, 49p.
Non diffusable
126852La traduction AADL-FIACRE. L'expérience TOPCASED
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, P.FARAIL, M.FILALI, P.GAUFILLET, F.VERNADAT
VERTICS, IRIT-UPS, EADS AIRBUS SA
Manifestation sans acte : Approches Formelles dans l'Assistance au Développement de Logiciels ( AFADL ) 2012 du 11 janvier au 13 janvier 2012, Grenoble (France), Janvier 2012, 51p. , N° 12773
Diffusable
129066Vérification formelle de spécifications AADL via FIACRE
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, M.FILALI, F.VERNADAT
IRIT-UPS, OLC
Manifestation sans acte : Ecole d'Eté Temps Réel (ETR'11), Brest (France), 29 Août - 2 Septembre 2011, 9p. , N° 11446
Diffusable
125705Mixed shared-distributed hash tables approaches for parallel state space construction
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
OLC
Manifestation avec acte : International Symposium on Parallel and Distributed Computing (ISPDC 2011) , Cluj-Napoca (Roumanie), 6-8 Juillet 2011, 8p. , N° 11460
Lien : http://hal.archives-ouvertes.fr/hal-00523188/fr/
Diffusable
Plus d'informations
Abstract
We propose an algorithm for parallel state space construction based on an original concurrent data structure, called a localization table, that aims at better spatial and temporal balance. Our proposal is close in spirit to algorithms based on distributed hash tables, with the distinction that states are dynamically assigned to processors; i.e. we do not rely on an a-priori static partition of the state space. In our solution, every process keeps a share of the global state space. Data distribution and coordination between processes is made through the localization table, that is a lockless, thread-safe data structure that approximates the set of states being processed. The localization table is used to dynamically assign newly discovered states and can be queried to return the identity of the processor that own a given state. With this approach, we are able to consolidate a network of local hash tables into an (abstract) distributed one without sacrificing memory affinity - data that are "logically connected" and physically close to each others - and without incurring performance costs associated to the use of locks to ensure data consistency. We evaluate the performance of our algorithm on different benchmarks and compare these results with other solutions proposed in the literature and with existing verification tools.
A dynamic, lock free data dictionary for parallel state space construction
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
OLC
Rapport LAAS N°10766, Décembre 2010, 12p.
Diffusable
123316A gnereral lock-free algorithm for parallel state space construction
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
OLC
Manifestation avec acte : International Workshop on Parallel and Distributed Methods in Verification (PDMC 2010), Twente (Pays Bas), 27 Septembre - 2 Octobre 2010, pp.8-16 , N° 10750
Lien : http://hal.archives-ouvertes.fr/hal-00473072/fr/
Diffusable
Plus d'informations
Abstract
Verification via model-checking is a very demanding activity in terms of computational resources. While there are still gains to be expected from algorithmic improvements, it is necessary to take advantage of the advances in computer hardware to tackle bigger models. Recent improvements in this area take the form of multiprocessor and multicore architectures with access to large memory space. We address the problem of generating the state space of finite state transition systems; often a preliminary step for modelchecking. We propose a novel algorithm for enumerative state space construction targeted at shared memory systems. Our approach relies on the use of two data structures: a shared Bloom filter to coordinate the state space exploration distributed among several processors and local dictionaries to store the states. The goal is to limit synchronization overheads and to increase the locality of memory access without having to make constant use of locks to ensure data integrity. Bloom filters have already been applied for the probabilistic verification of systems; they are compact data structures used to encode sets, but in a way that false positives are possible, while false negatives are not. We circumvent this limitation and propose an original multiphase algorithm to perform exhaustive, deterministic, state space generations. We assess the performance of our algorithm on different benchmarks and compare our results with the solution proposed by Inggs and Barringer.
Spécification des besoins RT-Fiacre
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, DDOOSE, M.FILALI, D.LE BOTLAN, P.MICHEL, M.PANTEL, F.VERNADAT
OLC, IRIT-UPS, ONERA, ONERA-CERT
Rapport de Contrat : FNRAE-QUARTEFT T1-06-A, Juillet 2010, 22p. , N° 10434
Diffusable
122073Real-time extensions for the fiacre modeling language
N.ABID, S.DAL ZILIO
OLC
Manifestation sans acte : International Summer School on MOdelling and VErifying parallel Processes (MOVEP' 2010), Aachen (Allemagne), 28 Juin - 2 Juillet 2010, 6p. , N° 10938
Lien : http://hal.archives-ouvertes.fr/hal-00593958/fr/
Diffusable
Plus d'informations
Abstract
We present our ongoing research on the extension of the Fiacre language with real-time con- structs and real-time verification patterns. Fiacre is a formal language with support for expressing concurrency and timing constraints; its goal is to act as an intermediate format for the formal verifica- tion of high-level modeling language, such as Architecture Description Languages or UML profiles for system modeling. Essentially, Fiacre is designed both as the target of model transformation en- gines from various languages, as well as the source language of compilers into verification toolboxes, namely Tina and CADP. Our motivations for extending Fiacre are to reduce the semantic gap between Fiacre and high-level description languages and to streamline our verification process.