Formal methods in model-based testing and verification
Contact: prof. Jüri Vain (juri.vain ätt ttu.ee, ICT-418)
Time and place
Lectures: Tuesdays 14:00, ICT-411
Spring 2015
- 17/02/2015
- Introduction to the seminar
- 03/03/2015
- Jishu Guin: cofoja - Contracts for Java (I)(https://code.google.com/p/cofoja/)
- 10/03/2015
- Deepak Pal: SMT solver Z3 (I)
- 17/03/2015
- Gert Kanter: KnowRob Knowledge processing system
- Jishu Guin: cofoja - Contracts for Java (II)
- 24/03/2015
- Natalya Berezovski: Maven - Project Management and Employment Tool (http://maven.apache.org/)
- KeY deductive verification tool I(http://www.key-project.org/)
- 31/03/2015
- Ago Luberg
- Jishu Guin:KeY verification system II(http://www.key-project.org/)
- 07/04/2015
- Tanel Tammet "Semantic web"
- Gert Kanter
- 14/04/2015
- Juhan Model-based testing with model programs: PyModel and NModel
- 21/04/2015
- Jaagup Irve
- 28/04/2015
- Jishu Guin:KeY verification system III (http://www.key-project.org/)
- 05/05/2015
- Deepak Pal: SMT solver Z3 (II) Z3 web(https://github.com/Z3Prover/z3/wiki)
- 12/05/2015
- Gert Kanter
- Evelin Halling
- 19/05/2015
- Jaagup Irve
- ...
Autumn 2014
- 17/09/2014 Introduction to the seminar
- 24/09/2014
- Jüri Vain "Provably correct test generation for online testing of timed systems"
- Andres Toom "A software product line approach for semantic specification of block libraries in dataflow language" [1]
Dataflow modelling languages such as SCADE or Simulink are the de-facto standard for the Model Driven Development of safety critical embedded control and command systems. Software is mainly being produced by Automated Code Generators whose correctness can only be assessed meaningfully if the input language semantics is well known. These semantics share a common part but are mainly defined through block libraries. The writing of a complete formal specification for the block libraries of the usual languages is highly challenging due to the high variability of the structure and semantics of each block. This contribution relates the use of software product line principles in the design of a domain specific language targeting the formal specification of block libraries. It summarises the advantages of this DSL regarding the writing, validation and formal verification of such specifications. These experiments have been carried out in the context of the GeneAuto embedded code generator project targeting Simulink and Scicos; and are being extended and applied in its follow up projects ProjetP and Hi-MoCo.
- 01/10/2014
- Jaagup Irve "Simulation modelling of robot swarms and emergent behaviour experiments (based on MSc Thesis)"
- 08/10/2014
- Deepak Pal "Model based distributed testing, literature survey"
- Jishu Guin "Abstraction learning: discussion on the reading list"
- 15/10/2014
- Gert Kanter & Evelin Halling "Joint report on European robot challenge"
- Jüri Vain "Towards context-sensitive dialogue with robot companion" (paper published in BEC 2014)[2]
- 22/10/2014
- Kristjan Liiva "A note on real quantifier elimination by virtual term substitution of unbounded degree"
We describe work in progress on constructing a complete implementation of Weispfenning's virtual term substitution method for real closed field formulas of unbounded degree. We build upon a recent high-performance library for computing over non-Archimedean real closed fields using Thom's Lemma.
- Kristjan Liiva "A note on real quantifier elimination by virtual term substitution of unbounded degree"
- 29/10/2014
- 05/11/2014
- Sergey Martynenko (Kharkiv National Aerospace University, Ukraine) "Hash Functions"
- 12/11/2014
- Andres Toom "Verification of Block Library specifications in deductive program verification environment Why" [3] Why3 home page
- Jishu Guin "Studies in knowledge representation of legal information – Discussion of selected papers from the reading list"
- 19/11/2014
- Jaagup Irve: "Swarm robotics: a review from the swarm engineering perspective" (Springer 2013) (part 1)
- 26/11/2014
- Seminar cancelled
- 03/12/2014
- Deepak Pal "Model Based Framework for Testing Distributed Systems"
- 10/12/2014
- Jishu Guin "Evaluation of a legal scenario using semantic networks in prolog – Assignment to demonstrate the evaluation of a simple legal scenario in prolog"
- Jaagup Irve: "[http://link.springer.com/article/10.1007/s11721-012-0075-2 Swarm robotics: a review from the swarm engineering
- 17/12/2014
- Andres Toom "Verification of model transformations"
- Deepak Pal "TBA"