scholarly journals Verified Lustre Normalization with Node Subsampling

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-25
Author(s):  
Timothy Bourke ◽  
Paul Jeanmaire ◽  
Basile Pesin ◽  
Marc Pouzet
Keyword(s):  
Embedded Systems ◽  
Code Generation ◽  
Reactive Systems ◽  
Type System ◽  
Theorem Prover ◽  
Correctness Proof ◽  
Assembly Code ◽  
Function Calls ◽  
End To End ◽  
Activation Conditions

Dataflow languages allow the specification of reactive systems by mutually recursive stream equations, functions, and boolean activation conditions called clocks. Lustre and Scade are dataflow languages for programming embedded systems. Dataflow programs are compiled by a succession of passes. This article focuses on the normalization pass which rewrites programs into the simpler form required for code generation. Vélus is a compiler from a normalized form of Lustre to CompCert’s Clight language. Its specification in the Coq interactive theorem prover includes an end-to-end correctness proof that the values prescribed by the dataflow semantics of source programs are produced by executions of generated assembly code. We describe how to extend Vélus with a normalization pass and to allow subsampled node inputs and outputs. We propose semantic definitions for the unrestricted language, divide normalization into three steps to facilitate proofs, adapt the clock type system to handle richer node definitions, and extend the end-to-end correctness theorem to incorporate the new features. The proofs require reasoning about the relation between static clock annotations and the presence and absence of values in the dynamic semantics. The generalization of node inputs requires adding a compiler pass to ensure the initialization of variables passed in function calls.

scholarly journals Verified Code Generation for Embedded Systems

2002 ◽  
Vol 65 (2) ◽  
pp. 19-36 ◽  
Author(s):  
Sabine Glesner ◽  
Rubino Geiß ◽  
Boris Boesler
Keyword(s):  
Embedded Systems ◽  
Code Generation

scholarly journals Design Methods and Processes for ML/DL models

2021 ◽  
Author(s):  
◽  
Meenu Mary John
Keyword(s):  
Embedded Systems ◽  
Design Methods ◽  
Key Factors ◽  
High Performing ◽  
Structured Design ◽  
Continuous Delivery ◽  
End To End ◽  
Access To Data ◽  
Structured Design Methods ◽  
Decentralized Architecture

Context: With the advent of Machine Learning (ML) and especially Deep Learning (DL) technology, companies are increasingly using Artificial Intelligence (AI) in systems, along with electronics and software. Nevertheless, the end-to-end process of developing, deploying and evolving ML and DL models in companies brings some challenges related to the design and scaling of these models. For example, access to and availability of data is often challenging, and activities such as collecting, cleaning, preprocessing, and storing data, as well as training, deploying and monitoring the model(s) are complex. Regardless of the level of expertise and/or access to data scientists, companies in all embedded systems domain struggle to build high-performing models due to a lack of established and systematic design methods and processes. Objective: The overall objective is to establish systematic and structured design methods and processes for the end-to-end process of developing, deploying and successfully evolving ML/DL models. Method: To achieve the objective, we conducted our research in close collaboration with companies in the embedded systems domain using different empirical research methods such as case study, action research and literature review. Results and Conclusions: This research provides six main results: First, it identifies the activities that companies undertake in parallel to develop, deploy and evolve ML/DL models, and the challenges associated with them. Second, it presents a conceptual framework for the continuous delivery of ML/DL models to accelerate AI-driven business in companies. Third, it presents a framework based on current literature to accelerate the end-to-end deployment process and advance knowledge on how to integrate, deploy and operationalize ML/DL models. Fourth, it develops a generic framework with five architectural alternatives for deploying ML/DL models at the edge. These architectural alternatives range from a centralized architecture that prioritizes (re)training in the cloud to a decentralized architecture that prioritizes (re)training at the edge. Fifth, it identifies key factors to help companies decide which architecture to choose for deploying ML/DL models. Finally, it explores how MLOps, as a practice that brings together data scientist teams and operations, ensures the continuous delivery and evolution of models.

scholarly journals Invariants and Robustness of BIP Models

10.29007/prxp ◽  
2018 ◽  
Author(s):  
Jan Olaf Blech ◽  
Thanh-Hung Nguyen ◽  
Michael Perin
Keyword(s):  
Embedded Systems ◽  
Higher Order ◽  
Theorem Prover ◽  
Important Goal ◽  
Invariant Generation ◽  
Execution Traces ◽  
Verification Tool ◽  
Verification Tools ◽  
Generation Mechanisms ◽  
Natural Way

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

scholarly journals End-to-end automated cache-timing attack driven by Machine Learning

10.29007/nwj8 ◽  
2019 ◽  
Author(s):  
Sebastien Carré ◽  
Victor Dyseryn ◽  
Adrien Facon ◽  
Sylvain Guilley ◽  
Thomas Perianin
Keyword(s):  
Neural Network ◽  
Language Processing ◽  
Relevant Information ◽  
Security Threats ◽  
Cache Memories ◽  
Function Calls ◽  
Timing Data ◽  
Timing Attack ◽  
End To End ◽  
Timing Attacks

Cache timing attacks are serious security threats that exploit cache memories to steal secret information.We believe that the identification of a sequence of operations from a set of cache-timing data measurements is not a trivial step when building an attack. We present a recurrent neural network model able to automatically retrieve a sequence of function calls from cache-timings. Inspired from natural language processing, our model is able to learn on partially labelled data. We use the model to unfold an end-to-end automated attack on OpenSSL ECDSA on the secp256k1 curve. Contrary to most research, we did not need human processing of the traces to retrieve relevant information.

scholarly journals Verified decision procedures for MSO on words based on derivatives of regular expressions

2015 ◽  
Vol 25 ◽  
Author(s):  
DMITRIY TRAYTEL ◽  
TOBIAS NIPKOW
Keyword(s):  
Code Generation ◽  
Decision Procedures ◽  
Theorem Prover ◽  
Regular Expressions ◽  
Data Types ◽  
Regular Structures ◽  
Derivatives Of ◽  
Second Order Logic ◽  
Generation Facility ◽  
Monadic Second Order Logic

AbstractMonadic second-order logic on finite words is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g., automata). This paper presents a verified functional decision procedure for MSO formulas that is not based on automata but on regular expressions. Functional languages are ideally suited for this task: regular expressions are data types and functions on them are defined by pattern matching and recursion and are verified by structural induction. Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions, an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Our results have been formalized and verified in the theorem prover Isabelle. Using Isabelle's code generation facility, this yields purely functional, formally verified programs that decide equivalence of MSO formulas.

Sign in / Sign up

Export Citation Format

Share Document