Showing 1–7 of 7 results for author: Serwe, W

Testing Resource Isolation for System-on-Chip Architectures

Authors: Philippe Ledent, Radu Mateescu, Wendelin Serwe

Abstract: Ensuring resource isolation at the hardware level is a crucial step towards more security inside the Internet of Things. Even though there is still no generally accepted technique to generate appropriate tests, it became clear that tests should be generated at the system level. In this paper, we illustrate the modeling aspects in test generation for resource isolation, namely modeling the behavi… ▽ More Ensuring resource isolation at the hardware level is a crucial step towards more security inside the Internet of Things. Even though there is still no generally accepted technique to generate appropriate tests, it became clear that tests should be generated at the system level. In this paper, we illustrate the modeling aspects in test generation for resource isolation, namely modeling the behavior and expressing the intended test scenario. We present both aspects using the industrial standard PSS and an academic approach based on conformance testing. △ Less

Submitted 27 March, 2024; originally announced March 2024.

Comments: In Proceedings MARS 2024, arXiv:2403.17862

Journal ref: EPTCS 399, 2024, pp. 129-168

Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing

Authors: Lina Marsso, Radu Mateescu, Lucie Muller, Wendelin Serwe

Abstract: We present two behavioral models of an autonomous vehicle and its interaction with the environment. Both models use the formal modeling language LNT provided by the CADP toolbox. This paper discusses the modeling choices and the challenges of our autonomous vehicle models, and also illustrates how formal validation tools can be applied to a single component or the overall vehicle. We present two behavioral models of an autonomous vehicle and its interaction with the environment. Both models use the formal modeling language LNT provided by the CADP toolbox. This paper discusses the modeling choices and the challenges of our autonomous vehicle models, and also illustrates how formal validation tools can be applied to a single component or the overall vehicle. △ Less

Submitted 18 March, 2022; originally announced March 2022.

Comments: In Proceedings MARS 2022, arXiv:2203.09299

Journal ref: EPTCS 355, 2022, pp. 60-117

Is CADP an Applicable Formal Method?

Authors: Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe

Abstract: CADP is a comprehensive toolbox implementing results of concurrency theory. This paper addresses the question, whether CADP qualifies as an applicable formal method, based on the experience of the authors and feedback reported by users. CADP is a comprehensive toolbox implementing results of concurrency theory. This paper addresses the question, whether CADP qualifies as an applicable formal method, based on the experience of the authors and feedback reported by users. △ Less

Submitted 15 November, 2021; originally announced November 2021.

Comments: In Proceedings AppFM 2021, arXiv:2111.07538

Journal ref: EPTCS 349, 2021, pp. 1-11

Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks

Authors: Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, Marc Renaudin

Abstract: Asynchronous circuits have several advantages for security applications, in particular their good resistance to attacks. In this paper, we report on experiments with modeling, at various abstraction levels, a patented asynchronous circuit for detecting physical attacks, such as cutting wires or producing short-circuits. Asynchronous circuits have several advantages for security applications, in particular their good resistance to attacks. In this paper, we report on experiments with modeling, at various abstraction levels, a patented asynchronous circuit for detecting physical attacks, such as cutting wires or producing short-circuits. △ Less

Submitted 28 April, 2020; originally announced April 2020.

Comments: In Proceedings MARS 2020, arXiv:2004.12403

Journal ref: EPTCS 316, 2020, pp. 200-239

Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation

Authors: John P. Gallagher, Rob van Glabbeek, Wendelin Serwe

Abstract: This volume contains the joint proceedings of MARS 2018, the third workshop on Models for Formal Analysis of Real Systems, and VPT 2018, the sixth international workshop on Verification and Program Transformation, held together on April 20, 2018 in Thessaloniki, Greece, as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software. MARS emphasises modelling over verifi… ▽ More This volume contains the joint proceedings of MARS 2018, the third workshop on Models for Formal Analysis of Real Systems, and VPT 2018, the sixth international workshop on Verification and Program Transformation, held together on April 20, 2018 in Thessaloniki, Greece, as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software. MARS emphasises modelling over verification. It aims at discussing the lessons learned from making formal methods for the verification and analysis of realistic systems. Examples are: (1) Which formalism is chosen, and why? (2) Which abstractions have to be made and why? (3) How are important characteristics of the system modelled? (4) Were there any complications while modelling the system? (5) Which measures were taken to guarantee the accuracy of the model? We invited papers that present full models of real systems, which may lay the basis for future comparison and analysis. An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. Alternative formal descriptions of the systems presented at this workshop are encouraged, which should foster the development of improved specification formalisms. VPT aims to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. These interactions have been beneficial in both directions. On the one hand, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, are applied with success to verification, in particular to the verification of infinite state and parameterized systems. On the other hand, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, are used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice. △ Less

Submitted 23 March, 2018; originally announced March 2018.

Journal ref: EPTCS 268, 2018

The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark

Authors: Hubert Garavel, Wendelin Serwe

Abstract: The multiway rendezvous introduced in Theoretical CSP is a powerful paradigm to achieve synchronization and communication among a group of (possibly more than two) processes. We illustrate the advantages of this paradigm on the production cell benchmark, a model of a real metal processing plant, for which we propose a compositional software controller, which is written in LNT and LOTOS, and makes… ▽ More The multiway rendezvous introduced in Theoretical CSP is a powerful paradigm to achieve synchronization and communication among a group of (possibly more than two) processes. We illustrate the advantages of this paradigm on the production cell benchmark, a model of a real metal processing plant, for which we propose a compositional software controller, which is written in LNT and LOTOS, and makes intensive use of the multiway rendezvous. △ Less

Submitted 19 March, 2017; originally announced March 2017.

Comments: In Proceedings MARS 2017, arXiv:1703.05812

Journal ref: EPTCS 244, 2017, pp. 230-270

Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard

Authors: Wendelin Serwe

Abstract: This paper presents two formal models of the Data Encryption Standard (DES), a first using the international standard LOTOS, and a second using the more recent process calculus LNT. Both models encode the DES in the style of asynchronous circuits, i.e., the data-flow blocks of the DES algorithm are represented by processes communicating via rendezvous. To ensure correctness of the models, several… ▽ More This paper presents two formal models of the Data Encryption Standard (DES), a first using the international standard LOTOS, and a second using the more recent process calculus LNT. Both models encode the DES in the style of asynchronous circuits, i.e., the data-flow blocks of the DES algorithm are represented by processes communicating via rendezvous. To ensure correctness of the models, several techniques have been applied, including model checking, equivalence checking, and comparing the results produced by a prototype automatically generated from the formal model with those of existing implementations of the DES. The complete code of the models is provided as appendices and also available on the website of the CADP verification toolbox. △ Less

Submitted 13 November, 2015; originally announced November 2015.

Comments: In Proceedings MARS 2015, arXiv:1511.02528

Journal ref: EPTCS 196, 2015, pp. 61-147