Modular xDSL Diagnosis

OBP2 is a specification and requirement verification environment, developed at ENSTA Bretagne. The main characteristics are:

  • the extensibility of the verification engine, which enables seamless integration of domain specific formalisms like UML, BPMN, TLA+, Fiacre;
  • the integration of domain-specific omniscient debugging with model-checking, which bridge the gap between early model diagnosis and formal verification;
  • the capacity to decompose the verification problem, which, based on the Context-aware Verification approach, addresses the scalability issues in the context of industrial scale verification.

OBP2

Context-aware Verification

The Context-aware Verification(CaV) provides a structured approach for capturing the verification problem through a number of independent verification contexts, which explicitly represent the restricted model behaviors along with the requirements to be verified. The model is decomposed in two components: the system- under-study (SUS) and the environment. While the SUS specification is viewed as a black-box that never changes during the verification, the environment model is decomposed in multiple interaction scenarios, captured through the CDL formalism. The verification contexts are created by associating to each interaction scenario the relevant properties that should be verified in each case. The verification process iteratively composes these contexts with the SUS to check the validity of the associated properties.

The CaV approach imposes a formal, methodical decomposition and classification of large requirements sets, a first step in overcoming the state-space explosion problem.

By limiting the scope of the system’s behavior, the complexity of the verification is reduced; the decoupling of the SUS from its environment eases the maintenance of the system by allowing the environment refinement in isolation.

Furthermore, the possibility to analyze the SUS with a partial environment model gives valuable insights on particular context-dependent behaviors, enabling the designers to better focus their verification efforts.

Last but not least, one important characteristic of the CaV methodology is the explicit identification of the acyclic behaviors, which allows to automatically decompose the verification problems in a divide-and-conquer manner and to apply the PastFree[ze] reachability algorithm.

The CaV approach is implemented in the freely available Observer-based Prover (OBP) toolkit.

CaV

Projects

Below are listed some of the projects I have been working on (reverse-chronological order).

VeriMoB [2018-2019]

Complex systems and systems of systems are specified using the NATO Architecture Framework (NAF) or DoD Architecture Framework (DoDAF). Business Process Model Notation (BPMN) is part of NAF and allows to describe the behavior of the different participants in the model. This notation is used by the French Army and its main suppliers to describe the interactions between participants involved in a mission. It is therefore important the models are correct.

The VeriMoB project is a research project financed by the Direction Générale de l’Armement (DGA), which aims at developing a tool that will help users to specify and verify their BPMN models. This tool covers three main aspects:

  • static verification for syntactical correcteness,
  • interactive execution for fine tuning (BPMN model animation),
  • verification of safety and vivacity properties (model-checking).

EASE4SE [2017-2019]

The NATO Architecture Framework (NAF) used the Business Process Model Notation (BPMN) for the high-level functional specification of complex System of Systems (SoS). The BPMN formalism is very expressive and focuses on the business level specification. During the SoS specification process a large number of stakeholders need to share a common operational vision on the dynamics of the system. For creating domain-specific operational simulations the French Army relies on discrete event simulation (DES) environments, such as DirectSim. While executable the level of discourse of a BPMN model remains very abstract, and disconnected from the operational reality captured using DES.

The EASE4SE project is a research project financed by the Direction Générale de l’Armement (DGA), which bridges the gap between the multiple operational views of a system and the overall functional coordination by providing a semantic-level connector between BPMN and DES.

DEPARTS [2013 - 2018]

References

  1. [1] C. Teodorov, L. Le Roux, Z. Drey, and P. Dhaussy, "Past-Free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis", Software Testing, Verification and Reliability, pp. n/a–n/a, Aug. 2016.
  2. [2] S. Heim, X. Dumas, E. Bonnafous, P. Dhaussy, C. Teodorov, and L. Leroux, "Model Checking of SCADE Designed Systems", in 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France, 2016.
  3. [3] C. Teodorov and P. Dhaussy, "Context-aware Verification", GDR GPL (Invited speaker). 2016.
  4. [4] C. Teodorov, P. Dhaussy, and L. Le Roux, "Environment-driven reachability for timed systems", International Journal on Software Tools for Technology Transfer, pp. 1–17, 2015.
  5. [5] C. Teodorov, L. L. Roux, and P. Dhaussy, "Modèle d’exécution de la plateforme de Simulation", DDASCA DEPARTS Livrable WP 4.1_1. 2015.
  6. [6] C. Teodorov, L. L. Roux, and P. Dhaussy, "Règles de tranformation ABCD vers Fiacre", DDASCA DEPARTS Livrable WP 4.1_2. 2015.
  7. [7] P. Dhaussy, L. Le Roux, and C. Teodorov, "Vérification formelle de propriétés : Application de l’outil OBP au cas d’étude CCS", Génie logiciel, vol. 109. C & S, Jun-2014.
  8. [8] F. Jouault, C. Teodorov, J. Delatour, L. Le Roux, and P. Dhaussy, "Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD", Génie logiciel, vol. 109. C & S, Jun-2014.
  9. [9] V. Ribaud, C. Teodorov, Z. Drey, L. Le Roux, and P. Dhaussy, "Techniques and Challenges for Trace Processing from a Model-Checking Perspective", in CISSE 2014, 2014.
  10. [10] C. Teodorov, L. Leroux, and P. Dhaussy, "Context-Aware Verification of a Cruise-Control System", in Model and Data Engineering, vol. 8748, Y. Ait Ameur, L. Bellatreche, and G. A. Papadopoulos, Eds. Springer International Publishing, 2014, pp. 53–64.
  11. [11] P. Dhaussy and C. Teodorov, "Context-Aware Verification of a Landing Gear System", in ABZ 2014: The Landing Gear Case Study, vol. 433, F. Boniol, V. Wiels, Y. Ait Ameur, and K.-D. Schewe, Eds. Springer International Publishing, 2014, pp. 52–65.

GeMOC [2013 - 2016]

References

  1. [1] J. Deantoni, I. P. Diallo, C. Teodorov, J. Champeau, and B. Combemale, "Towards a meta-language for the concurrency concern in DSLs", in Design, Automation Test in Europe Conference Exhibition (DATE), 2015, 2015, pp. 313–316.
  2. [2] J. Deantoni, P. I. Diallo, J. Champeau, B. Combemale, and C. Teodorov, "Operational Semantics of the Model of Concurrency and Communication Language", INRIA, Research Report RR-8584, Sep. 2014.
  3. [3] C. Teodorov, "Embedding Multiform Time Constraints in Smalltalk", in International Workshop on Smalltalk Technologies (IWST’14), 2014.

ARDyT [2011 - 2016]

References

  1. [1] S. Tleye, C. Teodorov, E. Fabiani, and L. Lagadec, "Phadeo: un environnement pour FPGA virtuel", in Conference en Parallelisme, Architecture et Systeme (COMPAS’15), 2015.
  2. [2] L. Lagadec, C. Teodorov, J.-C. L. Lann, D. Picard, and E. Fabiani, "Model-driven toolset for embedded reconfigurable cores: Flexible prototyping and software-like debugging", Science of Computer Programming, vol. 96, Part 1, pp. 156–174, 2014.

MoNaDe [2008 - 2011]

The integrated circuit industry continues to progress rapidly deepening the gap in between the technological breakthroughs and the electronic design automation industry. This gap is even more problematic in the context of physical design, the last automation level between applications and the technology. The challenges of meeting the physical and performance constraints necessitate innovation at the algorithmic level, and at the methodological level.

To address this problem we introduced a methodological approach to physical design automation relying on model-driven engineering. Based on the flexibility, and adaptability of the Smalltalk environment we propose an agile framework enabling fast physical design tool-flow prototyping [1].

We illustrate our approach using the Madeo FPGA toolkit as a legacy codebase that is incrementally changed to adopt the proposed model-driven development strategy.

References

  1. [1] C. Teodorov and L. Lagadec, "Virtual Prototyping of R2D Nasic Based FPGA", in Proceedings of the 2014 IEEE/ACM International Symposium on Nanoscale Architectures, New York, NY, USA, 2014, pp. 179–180.
  2. [2] C. Teodorov and L. Lagadec, "Model-driven physical-design automation for FPGAs: fast prototyping and legacy reuse", Software: Practice and Experience, vol. 44, no. 4, pp. 455–482, 2014.
  3. [3] C. Teodorov, "Model-Driven physical design for future architectures", Emerging Technologies meeting of GDR SoC-SiP (Invited speaker). Apr-2012.
  4. [4] C. Teodorov, "Model-Driven Physical-Design for Future Nanoscale Architectures", PhD thesis, Université de Bretagne Occidentale, 2011.
  5. [5] C. Teodorov and L. Lagadec, "MDE-based FPGA Physical Design. Fast Model-Driven Prototyping with Smalltalk", in International Workshop on Smalltalk Technologies, 2011.
  6. [6] C. Teodorov, P. Narayanan, L. Lagadec, and C. Dezan, "Regular 2D NASIC-based architecture and design space exploration", in Nanoscale Architectures (NANOARCH), 2011 IEEE/ACM International Symposium on, 2011, pp. 70–77.
  7. [7] C. Teodorov, L. Lagadec, and C. Dezan, "Max-Rate Pipeline with Regular NASIC-based Architecture Template", GDR SoC-SiP. 2011.
  8. [8] C. Teodorov, D. Picard, and L. Lagadec, "FPGA Physical-Design Automation using Model-Driven Engineering", in 6th International Workshop on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC’11), 2011.
  9. [9] C. Teodorov and L. Lagadec, "FPGA SDK for Nanoscale Architectures", in 6th International Workshop on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC’11), 2011.
  10. [10] C. Teodorov, "Comparing crossbar-based nano/CMOS architectures", in Design and Technology of Integrated Systems in Nanoscale Era (DTIS), 2010 5th International Conference on, 2010, pp. 1–6.
  11. [11] C. Dezan, C. Teodorov, L. Lagadec, M. Leuchtenburg, T. Wang, P. Narayanan, and A. Moritz, "Towards a framework for designing applications onto hybrid nano/CMOS fabrics", Microelectronics Journal, vol. 40, no. 4-5, pp. 656–664, 2009.
  12. [12] C. Teodorov, C. Dezan, and L. Lagadec, "Automatic Circuit Layout for Emerging Nanoscale Architectures", GDR SOC-SIP, Paris, France. Jun-2008.

Morpheus [2006-2009]

With the advances in circuit integration and communications, parallelism and concurrency are becoming the major concern in system design. At least two fields demonstrate clearly the strength of the evolutions in available hardware and related programming issues: - parallelism on chip, with multi-cores becoming the rule in general purpose computing, large FPGAs carrying processor cores and integration facilities, System-on-chip (SoC) that also have several cooperating processors or integrated functions. - parallelism out of the chip, with applications of intelligent sensor networks, or large scale, grid organization of computers The next generation of computing devices could even push the level of concurrency far beyond the current architectures due to nano-fabrics that are promising in terms of fabrication cost, power consumption, massive parallelism. If the arrival of parallelism has been predicted since a long time, it is unfortunate that current breakthroughs reveal an urgent need in concepts and tools for application contexts.

Morpheus proposes a technology breakthrough in the embedded computing field by integrating multiple reconfigurable cores into a heterogeneous SoC platform. To ease the exploitation of these novel architecture a

Project Details:

  • Coordinator: Philippe Bonnot, Thales Research & Technology, France
  • Period: January 2006 - September 2009
  • EU Program: 6th Framework Program
  • Global Budget: 16.57 M€
  • Global Funding by EU: 8.24 M€
  • Project partners:
    • Thales Research & Technology, France (coordinator)
    • Deutsche Thomson OHG, Germany,
    • Intracom SA Telecom Solutions, Greece
    • Alcatel-Lucent Deutschland AG, Germany
    • Thales Optronics SA, France
    • STMicroelectronics SRL, Italy
    • PACT XPP Technologies AG, Germany
    • Abound Logic, France
    • Associated Compiler Experts bv, The Netherlands
    • CriticalBlue, United Kingdom
    • Universitaet Karlsruhe, Germany
    • Technische Universiteit Delft, The Netherlands
    • Commissariat à l’Energie Atomique, France
    • Université de Bretagne Occidentale, France
    • Universita di Bologna, Italy
    • ARTTIC SAS, France
    • Technische Universitaet Braunschweig, Germany
    • Technische Universitaet Chemnitz, Germany

References

  1. [1] D. Picard, B. Pottier, and C. Teodorov, "Process System Modeling for RSoC", in 4th International Workshop on Reconfigurable Communication Centric System-on-Chips, 2008.
  2. [2] D. Picard, B. Pottier, and C. Teodorov, "Process Networks on Reconfigurable SoC", in Aether-Morpheus Workshop - Autumn School 2007 From reconfigurable to self-adaptative computing (AMWAS’07), Paris, France, 2007.
  3. [3] C. Teodorov, J. Knablein, and B. Pottier, "Quick Integration of High Level Tools in MORPHEUS: The case of SpecEdit", in Aether-Morpheus Workshop - Autumn School 2007 From reconfigurable to self-adaptative computing (AMWAS’07), Paris, France, 2007.
  4. [4] C. Teodorov, H. Dutta, and B. Pottier, "An Abstract Approach for System Description and Synthesis", First Workshop on Constraint Programming for Hardware Design, Rennes, France. Sep-2007.
  5. [5] C. Teodorov and B. Pottier, "SpecEdit Modeling and CDFG Translation", Université de Bretagne Occidentale, Aug. 2007.

Valmadeo [2005 - 2008]

Le projet de recherche VALMADEO a démarré le 7 Février 2005. Ce projet a pour objectif d’expertiser l’environnement de synthèse pour architectures recon gurables Madeo, développé dans le laboratoire Architectures et Systèmes de l’UBO. Le travail à e ectuer doit permettre la recherche d’architectures recon gurables originales pour les applications de communications numériques dans les domaines du codage canal (turbo-code) et plus généralement des traitements itératifs dans les récepteurs numériques. La validation des solutions architecturales obtenues dans l’environnement Madeo s’effectuera à l’aide de la plate-forme développée par l’ENST-Bretagne dans le cadre du projet PALMYRE. Le but de ce travail est de démontrer l’apport des caractéristiques spécifiques à Madeo par rapport au ot de conception classique pour les circuits reconfigurables.

Project details:

  • Coordinator:
  • Period: 2005 - 2008
  • Project Partners:
    • Telecom Bretagne, France
    • Université de Bretagne Occidentale, France

References

  1. [1] C. Dezan, T. Goubier, C. Teodorov, S. Yazdani, L. Lagadec, E. Fabiani, L. Le Dréau, Gueguen Loı̈c, C. Jégo, and B. Pottier, "Rapport et bilan pour le projet VALMADEO pour l’étape 3". Université de Bretagne Occidentale, Nov-2008.