Browsing by Author "Pereira, David"
Now showing 1 - 10 of 30
Results Per Page
Sort Options
- Abstract Timers and their Implementation onto the ARM Cor tex-M family of MCUsPublication . Lindgren, Per; Fresk, Emil; Lindner, Marcus; Lindner, Andreas; Pereira, David; Pinho, Luís MiguelReal-Time For the Masses (RTFM) is a set of languages andto ols b eing develop ed to facilitate emb edded software development and provide highly efficient implementations gearedto static verification. The RTFM-kernel is an architecturedesigned to provide highly efficient and predicable Stack Resource Policy based scheduling, targeting bare metal (singlecore) platforms.We contribute b eyond prior work by intro ducing a platform independent timer abstraction that relies on existingRTFM-kernel primitives. We develop two alternative implementations for the ARM Cortex-M family of MCUs: ageneric implementation, using the ARM defined SysTick-/DWT hardware; and a target sp ecific implementation, using the match compare/free running timers. While sacrificing generality, the latter is more flexible and may reduceoverall overhead. Invariants for correctness are presented,and metho ds to static and run-time verification are discussed. Overhead is b ound and characterized. In b oth casesthe critical section from release time to dispatch is less than2us on a 100MHz MCU. Queue and timer mechanisms aredirectly implemented in the RTFM-core language and canb e included in system-wide scheduling analysis.
- Contract Based Verification of IEC 61499Publication . Pereira, David; Pinho, Luís Miguel; Lindgren, Per; Lindner, MarcusThe IEC 61499 standard proposes an event driven execution model for component based (in terms of Function Blocks), distributed industrial automation applications. However, the standard provides only an informal execution semantics, thusin consequence behavior and correctness relies on the design decisions made by the tool vendor. In this paper we present the formalization of a subset of the IEC 61499 standard in order to provide an underpinning for the static verification of Function Block models by means of deductive reasoning. Specifically, we contribute by addressing verification at the component,algorithm, and ECC levels. From Function Block descriptions, enrichedwith formal contracts, we show that correctness of component compositions, as well as functional and transitional behavior can be ensured. Feasibility of the approach is demonstrated by manually encoding a set of representative use-cases in WhyML,for which the verification conditions are automatically derived (through the Why3 platform) and discharged (using automaticSMT-based solvers). Furthermore, we discuss opportunities and challenges towards deriving certified executables for IEC 61499 models.
- Deciding Kleene Algebra Terms Equivalence in CoqPublication . Pereira, David; Moreira, Nelma; Sousa, Simão Patrício Melo deThis paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.
- Design and Implementation of Secret Key Agreement for Platoon-based Vehicular Cyber-physical SystemsPublication . Li, Kai; Ni, Wei; Emami, Yousef; Shen, Yiran; Severino, Ricardo; Pereira, David; Tovar, EduardoIn a platoon-based vehicular cyber-physical system (PVCPS), a lead vehicle that is responsible for managing the platoon’s moving directions and velocity periodically disseminates control messages to the vehicles that follow. Securing wireless transmissions of the messages between the vehicles is critical for privacy and confidentiality of the platoon’s driving pattern. However, due to the broadcast nature of radio channels, the transmissions are vulnerable to eavesdropping. In this article, we propose a cooperative secret key agreement (CoopKey) scheme for encrypting/decrypting the control messages, where the vehicles in PVCPS generate a unified secret key based on the quantized fading channel randomness. Channel quantization intervals are optimized by dynamic programming to minimize the mismatch of keys. A platooning testbed is built with autonomous robotic vehicles, where a TelosB wireless node is used for onboard data processing and multihop dissemination. Extensive real-world experiments demonstrate that CoopKey achieves significantly low secret bit mismatch rate in a variety of settings. Moreover, the standard NIST test suite is employed to verify randomness of the generated keys, where the p-values of our CoopKey pass all the randomness tests. We also evaluate CoopKey with an extended platoon size via simulations to investigate the effect of system scalability on performance.
- A Domain Specific Language for Automotive Systems IntegrationPublication . Oliveira, Renato; Pereira, David; Maia, Cláudio; Santos, PedroDeveloping complex safe and secure Cyber-Physical Systems (CPS) applications for the automotive domain is typically a complex task, due to the criticality inherent to this domain. Considering such known complexity of the development process, we propose a novel solution that aims to provide a quasiautomatic1 integration process between the different components of such CPS systems via the support of a Domain Specific Language (DSL) that provides several views of the system, abstracting away the more technical implementation details, while imposing system properties and restrictions that have the potential to be formally verified (either statically or at run-time) during design, and facilitates the process of customization and quasi-automatic build and deployment processes. In this paper, we briefly analyze the tools that are available and that cover partially the characteristics of our envisioned DSL, describe its building blocks, and show how it can be applied in a small, yet sufficiently complex CPS application whose architecture is very close to what we may expect for the modern and future generation of CPS application in the automotive domain.
- End-to-End Response Time of 61499 Distributed Applications over Switched EthernetPublication . Lindgren, Per; Eriksson, Johan; Lindner, Marcus; Lindner, Andreas; Pereira, David; Pinho, Luís MiguelThe IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. For the deployment, each device may hold one or many logical resources, each consisting of a function block network with service interface blocks at the edges. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as messages). In this paper, we propose a low-complexity implementation technique allowing to assess end-to-end response times of event chains spanning over a set of networked devices. Based on a translation of IEC 61499 to RTFM1 -tasks and resources, the response time for each task in the system at the device-level can be derived using established scheduling techniques. In this paper, we develop a holistic method to provide safe end-to-end response times taking both intra and interdevice delivery delays into account. The novelty of our approach is the accuracy of the system scheduling overhead characterization. While the device-level (RTFM) scheduling overhead was discussed in previous works, the network-level scheduling overhead for switched Ethernets is discussed in this paper. The approach is generally applicable to a wide range of commercial offthe-shelf Ethernet switches without a need for expensive custom solutions to provide hard real-time performance. A behavior characterization of the utilized switch determines the guaranteed response times. As a use case, we study the implementation onto (single-core) Advanced RISC Machine (ARM)-cortex-based devices communicating over a switched Ethernet network. For the analysis, we define a generic switch model and an experimental setup allowing us to study the impact of network topology as well as 802.1Q quality of service in a mixed critical setting. Our results indicate that safe sub millisecond end-to-end resp
- Formal Contracts for Runtime Verification Support in the Ada Programming LanguagePublication . Matos Pedro, André; Pereira, David; Pinho, Luís Miguel; Sousa Pinto, JorgeStatic Verification is not sufficient to cope with many of the challenges of modern and future generation real-time embedded systems: • state-explosion problem of model-checking; • limited automation in deductive reasoning, even with recent advances in SAT and SMT solvers. • Most of the data important to certify a real-time embedded system is related to extra-functional properties: • Duration of tasks; • Energy consumption; • Temperature management; • Other cyber-physical properties. • Unfortunately, most of the extra functional data is only available and verifiable during execution time.
- Formal Verification of AADL Models Using UPPAALPublication . Gonçalves, Fernando; Pereira, David; Tovar, Eduardo; Becker, LeandroCyber-Physical Systems (CPS) are known to be highly complex systems which can be applied to a variety of different environments, covering both civil and military application domains. As CPS are typically complex systems, its design process requires strong guarantees that the specified functional and non-functional properties are satisfied on the designed application. Model-Driven Engineering (MDE) and high-level specification languages are a valuable asset to help the design and evaluation of such complex systems. However, when looking at the existing MDE tool-support, it is observed that there is still little support for the automated integration of formal verification techniques in these tools. Given that formal verification is necessary to ensure the levels of reliability required by safety critical CPS, this paper presents an approach that aims to integrate the Model Checking technique in the CPS design process for the purpose of correctly analyzing temporal and safety characteristics. A tool named ECPS Verifier was designed to support the model checking integration into the design process, providing the generation of timed automata models from high-levels specifications in AADL. The proposed method is illustrated by means of the design of an Unmanned Aerial Vehicle, from where we derive the timed automata models to be analyzed in the UPPAAL tool.
- Logic-based schedulability analysis for compositional hard real-time embedded systemsPublication . Pedro, André; Pereira, David; Pinho, Luís Miguel; Pinto, Jorge SousaOver the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for mis-interpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.
- MARS: a toolset for the safe and secure deployment of heterogeneous distributed systemsPublication . Nandi, Giann; Pereira, David; Proenca, José; Santos, José; Rodrigues, Lourenço A.; Lourenço, André; Tovar, EduardoThis work discusses the ongoing development of a toolset named MARS aimed to ease the process of safely deploying runtime verification monitors into distributed micro-ROS and ROS2 nodes. The work is motivated by a use case in the health and automotive domains and covers safety/security concerns around the manipulation of sensitive biometric data.
- «
- 1 (current)
- 2
- 3
- »