Lina Marsso - On model-based testing of GALS systems

10:30
Tuesday
10
Dec
2019
  • Thesis defence
Place: 
Organized by: 
Pierre Bouvier
Speaker: 
Lina Marsso
Teams: 

 

Jury: 

  • Holger Hermanns, Professor, Saarland University, (reviewer) 
  • Virginie Wiels, Senior researcher, ONERA, (reviewer) 
  • Roland Groz, Professor, Grenoble INP, (examiner) 
  • Eric Jenn, Engineer researcher, IRT SAINT-EXUPERY, (examiner) 
  • Dumitru Potop-Butucaru, Researcher (HdR ), Inria, (examiner) 
  • Radu Mateescu, DR2, INRIA, (PhD director) 
  • Ioannis Parissis, Professor, Laboratoire de Conception et d'Intégration de Systèmes (LCIS), (PhD co-director) 
  • Wendelin Serwe, Researcher, Inria, (PhD supervisor) 

This dissertation focuses on the model-based testing of GALS (Globally Asynchronous and Locally Synchronous) systems, which are inherently complex because of the combination of synchronous and asynchronous aspects. To cope with this complexity, we explore three directions: (1) techniques for synchronous components; (2) techniques for communication protocols between components; and (3) techniques for complete GALS systems, combining the results of the two previous directions. 

In the first direction, we explore formal techniques for the functional testing of synchronous components. As a case-study, we reconsider the Message Authenticator Algorithm (MAA), a pioneering cryptographic function designed in the mid-80s, and formalize it as a synchronous dataflow. The modeling and validation of the MAA enabled us to discover various mistakes in prior (informal and formal) specifications of the MAA, the test vectors and code of the ISO 1987 and ISO 1990 standards, and in compilers and verification tools used by us. 

In the second direction, we explore the formalization and the functional testing of a communication protocol. As a case-study, we reconsider the formalization of the Transport Layer Security (TLS) handshake, a protocol responsible for the authentication and exchange of keys necessary to establish or resume a secure communication. Our model of the TLS version 1.3 has been validated by an approach using our new on-the-fly conformance test case generation tool, named TESTOR, developed on top of the CADP toolbox. TESTOR explores the model and generates automatically a set of controllable test cases or a complete test graph (CTG) to be executed on a physical implementation of the system. 

In the third direction, we propose a testing methodology for GALS systems combining the two previous directions. We leverage the conformance test generation for asynchronous systems to automatically derive realistic scenarios (inputs constraints and oracles), which are necessary ingredients for the unit testing of individual synchronous components, and are difficult and error-prone to design manually. Thus, our methodology integrates (1) synchronous and asynchronous concurrent models; (2) functional unit testing and behavioral conformance testing; and (3) various formal methods and their tools. 

We illustrate our methodology on a simple, but relevant example inspired by autonomous cars.