Search

Your search keyword '"Nadezhda Baklanova"' showing total 7 results
Start Over Author "Nadezhda Baklanova"
7 results on '"Nadezhda Baklanova"'

6. Coding, Executing and Verifying Graph Transformations with small-tALCQe

Author

Nadezhda Baklanova, Jon Haël Brenas, Amani Makhlouf, Christian Percebois, Martin Strecker, Hanh Nhi Tran, Systerel, Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Centre National de la Recherche Scientifique (CNRS), Advancing Rigorous Software and System Engineering (IRIT-ARGOS), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), SYSTEREL (FRANCE), Université de Grenoble (FRANCE), and Institut de Recherche en Informatique de Toulouse - IRIT (Toulouse, France)

Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Modélisation et simulation, Systèmes embarqués, Interface homme-machine, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Graph transformations, Counterexample generation, Program testing, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Architectures Matérielles, Program verification, Cryptographie et sécurité, Génie logiciel, Software analysis, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC]
Abstract

International audience; This paper gives an overview of small-tALCQe, an experi-mental programming environment for a graph transformation languagethat is based on the ALCQ description logic. small-tALCQe not onlyallows developers coding and executing graph transformations but alsoassists them in analyzing and verifying their codes. We describe the com-ponents that make up small-tALCQe: the transformation language itself,the compiler for generating executable transformations, the code ana-lyzers and the prover for reasoning about transformations. All of theminteract under the hood of an Eclipse user interface to provide differentlevels of assistance for achieving correct graph transformations.

Published
2016

7. Abstraction and Verification of Properties of a Real-Time Java

Author

Martin Strecker, Nadezhda Baklanova, Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Centre National de la Recherche Scientifique - CNRS (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, and Institut National Polytechnique de Toulouse - INPT (FRANCE)

Subjects
Model checking, [INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], Java, Scala, Computer science, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], computer.software_genre, Interface homme-machine, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Real time Java, Architectures Matérielles, 020204 information systems, Multithreading, 0202 electrical engineering, electronic engineering, information engineering, Génie logiciel, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], computer.programming_language, Uppaal, Programming language, strictfp, Resource sharing conflict, Deadlock, Modélisation et simulation, Java concurrency, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Systèmes embarqués, Shared resource, Timed automaton, Cryptographie et sécurité, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, computer, Java Modeling Language
Abstract

International audience; We present a tool for analysing resource sharing conflicts in multithreaded Java programs. Java programs are translated to timed automata models verified afterwards by the Uppaal model checker. Analysed programs are annotated with timing information indicating the execution duration of a particular statement. Based on the timing information, the analysis of execution paths is performed, which gives an answer whether resource sharing conflicts are possible in a multithreaded Java program. If the analysis succeeds, resource locks may be eliminated from the Java program.

Published
2013

Catalog

Books, media, physical & digital resources
See catalog results