Author details
Author's Published Works
Author details
Showing 1-11 of 11 results
- Sort
Filter Results
Show
Sort By
Results
CertiCAN: A Tool for the Coq Certification of CAN Analysis Results
Pascal Fradet;Xiaojie Guo;Jean-François Monin;Sophie Quinton
2019 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)
Year: 2019 | Conference Paper |
Cited by: Papers (2)
This paper introduces CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is light-weight and flexible compared to tool certification, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques,...Show More
RDF: Reconfigurable Dataflow
Pascal Fradet;Alain Girault;Ruby Krishnaswamy;Xavier Nicollin;Arash Shafiei
2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)
Year: 2019 | Conference Paper |
Cited by: Papers (5)
Dataflow Models of Computation (MoCs) are widely used in embedded systems, including multimedia processing, digital signal processing, telecommunications, and automatic control. In a dataflow MoC, an application is specified as a graph of actors connected by FIFO channels. One of the most popular dataflow MoCs, Synchronous Dataflow (SDF), provides static analyses to guarantee boundedness and liven...Show More
A Generic Coq Proof of Typical Worst-Case Analysis
Pascal Fradet;Maxime Lesourd;Jean-François Monin;Sophie Quinton
This paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. TWCA was originally introduced for systems with fixed priority preemptive (FPP) schedulers and has since been extended to fixed-priority nonpreemptive (FPNP) and earliest-deadline-first (EDF) schedulers. Our generic analysis is based on an abstract model ...Show More
Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets
Xiaojie Guo;Sophie Quinton;Pascal Fradet;Jean-Francois Monin
This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq's extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a ...Show More
Symbolic Buffer Sizing for Throughput-Optimal Scheduling of Dataflow Graphs
2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)
Year: 2016 | Conference Paper |
Cited by: Papers (6)
The synchronous dataflow model is widely used to design real-time streaming applications which must assure a minimum quality-of-service. A benefit of that model is to allow static analyses to predict and guarantee timing (e.g., throughput) and buffering requirements of an application. Performance analyses can either be performed at compile time (for design space exploration) or at run-time (for re...Show More
Formal verification of automatic circuit transformations for fault-tolerance
2015 Formal Methods in Computer-Aided Design (FMCAD)
Year: 2015 | Conference Paper |
Cited by: Papers (1)
We present a language-based approach to certify fault-tolerance techniques for digital circuits. Circuits are expressed in a gate-level Hardware Description Language (HDL), fault-tolerance techniques are described as automatic circuit transformations in that language, and fault-models are specified as particular semantics of the HDL. These elements are formalized in the Coq proof assistant and the...Show More
Time-redundancy transformations for adaptive fault-tolerant circuits
2015 NASA/ESA Conference on Adaptive Hardware and Systems (AHS)
Year: 2015 | Conference Paper |
Cited by: Papers (1)
We present a novel logic-level circuit transformation technique for the automatic insertion of fault-tolerance properties. The transformations, based on time-redundancy, allow dynamic changes of the level of redundancy without interrupting the computation. The proposed concept of dynamic time redundancy permits adaptive circuits whose fault-tolerance properties can be “on-the-fly” traded-off for t...Show More
Verification-guided voter minimization in triple-modular redundant circuits
2014 Design, Automation & Test in Europe Conference & Exhibition (DATE)
Year: 2014 | Conference Paper |
Cited by: Papers (1)
We present a formal approach to minimize the number of voters in triple-modular redundant sequential circuits. Our technique actually works on a single copy of the circuit and considers a user-defined fault model (under the form “at most 1 bit-flip every k clock cycles”). Verification-based voter minimization guarantees that the resulting circuit (i) is fault tolerant to the soft-errors defined by...Show More
BPDF: A statically analyzable dataflow model with integer and boolean parameters
2013 Proceedings of the International Conference on Embedded Software (EMSOFT)
Year: 2013 | Conference Paper |
Cited by: Papers (31)
Dataflow programming models are well-suited to program many-core streaming applications. However, many streaming applications have a dynamic behavior. To capture this behavior, parametric dataflow models have been introduced over the years. Still, such models do not allow the topology of the dataflow graph to change at runtime, a feature that is also required to program modern streaming applicatio...Show More
SPDF: A schedulable parametric data-flow MoC
2012 Design, Automation & Test in Europe Conference & Exhibition (DATE)
Year: 2012 | Conference Paper |
Cited by: Papers (20)
Dataflow programming models are suitable to express multi-core streaming applications. The design of high-quality embedded systems in that context requires static analysis to ensure the liveness and bounded memory of the application. However, many streaming applications have a dynamic behavior. The previously proposed dataflow models for dynamic applications do not provide any static guarantees or...Show More
Specialized Aspect Languages Preserving Classes of Properties
2008 Sixth IEEE International Conference on Software Engineering and Formal Methods
Year: 2008 | Conference Paper |
Aspect oriented programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In previous work, we have identified categories of aspects that preserve classes of temporal properties. We have formally proved that, for any program,the weaving of any aspect in a category preserves all properties in the ...Show More
IEEE Account
Purchase Details
Profile Information
Need Help?
- US & Canada: +1 800 678 4333
- Worldwide: +1 732 981 0060
- Contact & Support
- About IEEE Xplore
- Contact Us
- Help
- Accessibility
- Terms of Use
- Nondiscrimination Policy
- Sitemap
- Privacy & Opting Out of Cookies
A not-for-profit organization, IEEE is the world's largest technical professional organization dedicated to advancing technology for the benefit of humanity.
© Copyright 2025 IEEE - All rights reserved. Use of this web site signifies your agreement to the terms and conditions.