Browsing by Author "Lindner, Marcus"
Now showing 1 - 4 of 4
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.
- 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
- Towards Certified Compilation of RTFM-core ApplicationsPublication . Pereira, David; Pinho, Luís Miguel; Lindgren, Per; Lindner, MarcusConcurrent programming is dominated by thread based solutions with lock based critical sections. Careful attention has to be paid to avoid race and deadlock conditions. Real-Time for The Masses (RTFM) takes an alternative language approach, introducing tasks and named critical sections (via resources) natively in the RTFM-core language. RTFM-core programs can be compiled to native C-code, and efficiently executed onto single-core platforms under the Stack Resource Policy (SRP) by the RTFM-kernel. In this paper we formally define the well-formedness criteria for SRP based resource management, and develop a certified (formally proven) implementation of the corresponding compilation from nested critical sections of the input RTFM-core program to a resulting flat sequence of primitive operations and scheduling primitives. Moreover we formalise the properties for resource ceilings under SRP and develop a certified algorithm for their computation. The feasibility of the described approach is shown through the adoption of the Why3 platform, which allows the necessary verification conditions to be automatically generated and discharged through a variety of automatic external SMT-solvers and interactive theorem provers. Moreover, Why3 supports the extraction of certified Ocaml code for proven implementations in WhyML. As a proof of concept the certified extracted development is demonstrated on an example system.