Change search
Link to record
Permanent link

Direct link
BETA
Lindgren, Per
Publications (10 of 90) Show all publications
Lindner, M., Aparicio, J. & Lindgren, P. (2019). Concurrent Reactive Objects in Rust Secure by Construction. Ada User Journal, 40(1)
Open this publication in new window or tab >>Concurrent Reactive Objects in Rust Secure by Construction
2019 (English)In: Ada User Journal, ISSN 1381-6551, Vol. 40, no 1Article in journal (Refereed) Published
Abstract [en]

Embedded systems of the IoT era face the software developer with requirements on a mix of resource efficiency, real-time, safety, and security properties. As of today, C/C++ programming dominates the mainstream of embedded development, which leaves ensuring system wide properties mainly at the hands of the programmer. We adopt a programming model and accompanying framework implementation that leverages on the memory model, type system, and zero-cost abstractions of the Rust language. Based on the outset of reactivity, a software developer models a system in terms of Concurrent Reactive Objects (CROs) hierarchically grouped into Concurrent Reactive Components (CRCs) with communication captured in terms of time constrained synchronous and asynchronous messages. The developer declaratively defines the system, from which a static system instance can be derived and analyzed. A system designed in the proposed CRC framework has the outstanding properties of efficient, memory safe, race-, and deadlock-free preemptive (single-core) execution with predictable real-time properties. In this paper, we further explore the Rust memory model and the CRC framework towards systems being secure by construction. In particular, we show that permissions granted can be freely delegated without any risk of leakage outside the intended set of components. Moreover, the model guarantees permissions to be authentic, i.e., neither manipulated nor faked. Finally, the model guarantees permissions to be temporal, i.e., never to outlive the granted authority. We believe and argue that these properties offer the fundamental primitives for building secure by construction applications and demonstrate its feasibility on a small case study, a wireless autonomous system based on an ARM Cortex M3 target.

Place, publisher, year, edition, pages
Ada Language UK Ltd., 2019
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-71246 (URN)2-s2.0-85067078450 (Scopus ID)
Note

Validerad;2019;Nivå 1;2019-04-09 (inah)

Available from: 2018-10-17 Created: 2018-10-17 Last updated: 2019-06-28Bibliographically approved
Lindner, M., Aparicio, J., Tjäder, H., Lindgren, P. & Eriksson, J. (2018). Hardware-in-the-loop based WCET analysis with KLEE. In: 2018 IEEE 23RD INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA): . Paper presented at 23rd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2018) Politecnico Torino,Italy , Sep 04-07, 2018 (pp. 345-352). Piscataway, NJ: IEEE
Open this publication in new window or tab >>Hardware-in-the-loop based WCET analysis with KLEE
Show others...
2018 (English)In: 2018 IEEE 23RD INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), Piscataway, NJ: IEEE, 2018, p. 345-352Conference paper, Published paper (Refereed)
Abstract [en]

C programming dominates the mainstream of embedded development as of today. To aid the development, hardware abstractions, libraries, kernels, and light-weight operating systems are commonplace. However, these typically offer little or no help to automatic worst-case execution time (WCET) estimation, and thus manual test and measurement based approaches remain the de facto standard. For this paper, we take the outset from the Real-Time For the Masses (RTFM) framework, which is developed to facilitate embedded software development for IoT devices and provides highly efficient implementations, suitable to the mainstream of embedded system design. Although the Rust language plays currently a minor part in embedded development, we believe its properties add significant improvements and thus implement our RTFM framework in Rust. We present an approach to worst-case execution time estimation in the context of RTFM tasks and critical sections, which renders sufficient information for further response time and schedulability analysis. We introduce our test bench, which utilizes the KLEE tool for automatic test vector generation and subsequently performs cycle accurate hardware-in-the-loop measurements of the generated tests. The approach is straightforward and fully automatic. Our solution bridges the gap in between measurement based and static analysis methods for WCET estimation. We demonstrate the feasibility of the approach on a running example throughout the paper and conclude with a discussion on its implications and limitations.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE, 2018
Series
IEEE International Conference on Emerging Technologies and Factory Automation-ETFA, ISSN 1946-0740
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-71247 (URN)10.1109/ETFA.2018.8502510 (DOI)000449334500042 ()2-s2.0-85057245110 (Scopus ID)978-1-5386-7108-5 (ISBN)
Conference
23rd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2018) Politecnico Torino,Italy , Sep 04-07, 2018
Available from: 2018-10-17 Created: 2018-10-17 Last updated: 2019-02-27Bibliographically approved
Aparicio Rivera, J., Lindner, M. & Lindgren, P. (2018). Heapless: Dynamic Data Structures without Dynamic Heap Allocator for Rust. In: 2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN): . Paper presented at 16th International Conference on Industrial Informatics (INDIN), Porto, Portugal, 18-20 July 2018 (pp. 87-94). Piscataway, NJ: IEEE, Article ID 8472097.
Open this publication in new window or tab >>Heapless: Dynamic Data Structures without Dynamic Heap Allocator for Rust
2018 (English)In: 2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), Piscataway, NJ: IEEE, 2018, p. 87-94, article id 8472097Conference paper, Published paper (Refereed)
Abstract [en]

Dynamic memory management is typically implemented using a global memory allocator, which may negatively impact the performance, reliability, and predictability of a program; in effect standards around safety-critical applications often discourage or even disallow dynamic memory management. This paper presents heapless, a collection of dynamic data structures (for vectors, strings, and circular buffers) that can be either stack or statically allocated, thus free of global allocator dependencies. The proposed data structures for vectors and strings closely mimic the Rust standard library implementations while adding support to gracefully handling cases of capacity exceedance. Our circular buffers act as queues and allowing channel like usage (by splitting). The Rust memory model together with the ability of local reasoning on memory requirements (brought by heapless) facilitates establishing robustness/safety guarantees and minimize attack surfaces of (industrial) IoT systems. We show that the heapless data structures are highly efficient and have predictable performance, thus suitable for hard real-time applications. Moreover, in our implementation heapless data structures are non-relocatable allowing mapping to hardware, useful, e.g., to DMA transfers. The feasibility, performance, and advantages of heapless are demonstrated by implementing a JSON serialization and de-serialization library for an ARM Cortex-M based IoT platform.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE, 2018
Series
IEEE International Conference on Industrial Informatics INDIN, ISSN 1935-4576, E-ISSN 2378-363X
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-71248 (URN)10.1109/INDIN.2018.8472097 (DOI)000450180200012 ()2-s2.0-85055553702 (Scopus ID)978-1-5386-4829-2 (ISBN)
Conference
16th International Conference on Industrial Informatics (INDIN), Porto, Portugal, 18-20 July 2018
Available from: 2018-10-17 Created: 2018-10-17 Last updated: 2019-01-15Bibliographically approved
Lindner, M., Aparicio, J. & Lindgren, P. (2018). No Panic! Verification of Rust Programs by Symbolic Execution. In: : . Paper presented at 16th International Conference on Industrial Informatics (INDIN), Porto, Portugal, 18-20 July 2018 (pp. 108-114). Piscataway, NJ: IEEE, Article ID 8471992.
Open this publication in new window or tab >>No Panic! Verification of Rust Programs by Symbolic Execution
2018 (English)Conference paper, Published paper (Refereed)
Abstract [en]

The Rust language stands out with a type system and underlying memory model targeting memory safety. The accompanying rustc compiler is typically able to statically prove the safety conditions and accept or reject input programs accordingly. However, e.g., cases of raw array indexing are in general out of reach for static analysis and promoted to runtime verification rendering executables with partial correctness guarantees (aborting with a panic on safety violations). For safety-critical applications, this requires proper panic handling, which is by itself a hard problem. Moreover, runtime verification may be undesirable for performance reasons and hence calling for stronger methods to static program analysis. In this paper, we take the approach of symbolic execution and propose a generic contract based verification process for programs written in Rust. For the verified properties (assertions), the program is both safe and panic free. Besides correctness, this implies further performance improvements as code for runtime verification can be safely dropped. We demonstrate the feasibility of the approach by adopting the KLEE symbolic execution engine to analyze LLVM bitcode extracted from Rust programs and libraries under verification and discuss its implications and limitations.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE, 2018
Series
IEEE International Conference on Industrial Informatics INDIN, ISSN 1935-4576, E-ISSN 2378-363X
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-71249 (URN)10.1109/INDIN.2018.8471992 (DOI)000450180200015 ()2-s2.0-85055511267 (Scopus ID)978-1-5386-4829-2 (ISBN)978-1-5386-4830-8 (ISBN)
Conference
16th International Conference on Industrial Informatics (INDIN), Porto, Portugal, 18-20 July 2018
Available from: 2018-10-17 Created: 2018-10-17 Last updated: 2019-02-27Bibliographically approved
Lindgren, P., Lindner, M., Pereira, D. & Pinho, L. M. (2017). Contract Based Verification of IEC 61499. In: IEEE International Conference on Industrial Informatics (INDIN): . Paper presented at IEEE International Conference on Industrial Informatics 2016 (INDIN 2016), Poitiers, France, 18-21 July 2016 (pp. 132-141). Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), Article ID 7819147.
Open this publication in new window or tab >>Contract Based Verification of IEC 61499
2017 (English)In: IEEE International Conference on Industrial Informatics (INDIN), Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017, p. 132-141, article id 7819147Conference paper, Published paper (Refereed)
Abstract [en]

The IEC 61499 standard proposes an event drivenexecution model for component based (in terms of FunctionBlocks), distributed industrial automation applications. However,the standard provides only an informal execution semantics, thusin consequence behavior and correctness relies on the designdecisions made by the tool vendor. In this paper we presentthe formalization of a subset of the IEC 61499 standard inorder to provide an underpinning for the static verification ofFunction 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 componentcompositions, as well as functional and transitional behaviorcan be ensured. Feasibility of the approach is demonstrated bymanually 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 andchallenges towards deriving certified executables for IEC 61499models.

Place, publisher, year, edition, pages
Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017
Series
IEEE International Conference on Industrial Informatics INDIN, ISSN 1935-4576
National Category
Embedded Systems
Research subject
Industrial Electronics
Identifiers
urn:nbn:se:ltu:diva-59756 (URN)10.1109/INDIN.2016.7819147 (DOI)000393551200017 ()2-s2.0-85012929062 (Scopus ID)9781509028702 (ISBN)
Conference
IEEE International Conference on Industrial Informatics 2016 (INDIN 2016), Poitiers, France, 18-21 July 2016
Available from: 2016-10-14 Created: 2016-10-14 Last updated: 2017-11-24Bibliographically approved
Lindgren, P., Eriksson, J., Lindner, M., Lindner, A., Pereira, D. & Pinho, L. M. (2017). End-to-End Response Time of 61499 Distributed Applications over Switched Ethernet. IEEE Transactions on Industrial Informatics, 13(1), 287-297
Open this publication in new window or tab >>End-to-End Response Time of 61499 Distributed Applications over Switched Ethernet
Show others...
2017 (English)In: IEEE Transactions on Industrial Informatics, ISSN 1551-3203, E-ISSN 1941-0050, Vol. 13, no 1, p. 287-297Article in journal (Refereed) Published
Abstract [en]

The 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 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 inter-device 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 COTS 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) ARMcortex 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 response times can be obtained using the proposed approach.

Place, publisher, year, edition, pages
IEEE, 2017
National Category
Embedded Systems
Research subject
Embedded Systems
Identifiers
urn:nbn:se:ltu:diva-60286 (URN)10.1109/TII.2016.2626463 (DOI)000395874400029 ()2-s2.0-85013444377 (Scopus ID)
Note

Validerad; 2017; Nivå 2; 2017-02-21 (rokbeg)

Available from: 2016-11-10 Created: 2016-11-10 Last updated: 2019-02-27Bibliographically approved
Blech, J. O., Lindgren, P., Pereira, D., Vyatkin, V. & Zoitl, A. (2016). A Comparison of Formal Verification Approaches for IEC 61499. In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016. Paper presented at 21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016. Piscataway, NJ: IEEE conference proceedings, Article ID 7733636.
Open this publication in new window or tab >>A Comparison of Formal Verification Approaches for IEC 61499
Show others...
2016 (English)In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016, Piscataway, NJ: IEEE conference proceedings, 2016, article id 7733636Conference paper, Published paper (Refereed)
Abstract [en]

Engineering and computer science have come up with a variety of techniques to increase the confidence in systems, increase reliability, facilitate certification, improve reuse and maintainability, improve interoperability and portability. Among them are various techniques based on formal models to enhance testing, validation and verification. In this paper, we are concentrating on formal verification both at runtime and design time of a system. Formal verification of a system property at design time is the process of mathematically proving that the property indeed holds. At runtime, one can check the validity of the property and report deviations by monitoring the system execution. Formal verification relies on semantic models, descriptions of the system and its properties. We report on ongoing verification work and present two different approaches for formal verification of IEC 61499-based programs. We provide two examples of ongoing work to exemplify the design and the runtime verification approaches

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE conference proceedings, 2016
Series
I E E E International Conference on Emerging Technologies and Factory Automation. Proceedings, ISSN 1946-0740
National Category
Embedded Systems Computer Sciences
Research subject
Embedded System; Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-60319 (URN)10.1109/ETFA.2016.7733636 (DOI)000389524200143 ()2-s2.0-84996483346 (Scopus ID)978-1-5090-1314-2 (ISBN)978-1-5090-1313-5 (ISBN)
Conference
21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016
Available from: 2016-11-11 Created: 2016-11-11 Last updated: 2018-01-13Bibliographically approved
Lindgren, P., Fresk, E., Lindner, M., Lindner, A., Pereira, D. J. & Pinho, L. M. (2016). Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs (ed.). Paper presented at Embedded Systems Week 2015 : 04/10/2015 - 09/10/2015. , 13(1)
Open this publication in new window or tab >>Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs
Show others...
2016 (English)In: Vol. 13, no 1Article in journal (Refereed) Published
Abstract [en]

Real-Time For the Masses (RTFM) is a set of languages andtools being developed to facilitate embedded software developmentand provide highly ecient implementations gearedto static verication. The RTFM-kernel is an architecturedesigned to provide highly ecient and predicable Stack ResourcePolicy based scheduling, targeting bare metal (singlecore)platforms.We contribute by introducing a platform independent timerabstraction that relies on existing RTFM-kernel primitives.We develop two alternative implementations for the ARMCortex-M family of MCUs: a generic implementation, usingthe ARM dened SysTick/DWT hardware; and a targetspecic implementation, using the match compare/free runningtimers. While sacricing generality, the latter is moreexible and may reduce overall overhead. Invariants for correctnessare presented, and methods to static and run-timeverication are discussed. Overhead is bound and characterized.In both cases the critical section from release timeto dispatch is less than 2us on a 100MHz MCU. Queue andtimer mechanisms are directly implemented in the RTFMcorelanguage (-core in the following) and can be includedin system-wide scheduling analysis.

National Category
Embedded Systems Control Engineering
Research subject
Embedded System; Control Engineering
Identifiers
urn:nbn:se:ltu:diva-39517 (URN)e4d7eb1b-7017-41d4-860e-3fba546502ca (Local ID)e4d7eb1b-7017-41d4-860e-3fba546502ca (Archive number)e4d7eb1b-7017-41d4-860e-3fba546502ca (OAI)
Conference
Embedded Systems Week 2015 : 04/10/2015 - 09/10/2015
Note

Godkänd;2016;20151216 (maalin);Konferensartikel i tidskrift;Bibliografisk uppgift: Special Issue on 5th Embedded Operating Systems Workshop (EWiLi 2015)

Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2018-05-29Bibliographically approved
Lindner, M., Lindner, A. & Lindgren, P. (2016). RTFM-core: course in compiler construction. The SIGBED Review, 14(1), 29-36
Open this publication in new window or tab >>RTFM-core: course in compiler construction
2016 (English)In: The SIGBED Review, ISSN 1551-3688, Vol. 14, no 1, p. 29-36Article in journal (Refereed) Published
Abstract [en]

The course in Compiler Construction is part of the Computer Science masters program at Luleå University of Technology (LTU). Since the fall of 2014, the course is given by the Embedded Systems group. This paper outlines the course syllabus and its relation to CPS/IoT and embedded systems in general. In particular, the course introduces domain specific language design with the outset from the imperative RTFM-core language. Students are exposed to design choices for the language, spanning from programming model, compiler design issues, back-end tools, and even runtime environments. The intention is to give a holistic perspective and motivate the use of compilation techniques towards robust, efficient, and verifiable (embedded) software. Of course, developing basic skills is not overlooked and as part of the laboratory assignments, students extend the min-imalistic Object Oriented language RTFM-cOOre and develop the compiler accordingly targeting the RTFM-core language as an intermediate representation. As the RTFM-core/-cOOre compilers are implemented using OCaml/Men-hir, the students are also exposed to functional languages and to their advantages in the context of compiler construction. However, for their own development they may choose alternative design tools and languages. This gives us the opportunity to review and correlate achievements and efficiency to the choice of tools and languages and it is an outset for future course development.

National Category
Embedded Systems
Research subject
Embedded System
Identifiers
urn:nbn:se:ltu:diva-61641 (URN)10.1145/3036686.3036690 (DOI)
Available from: 2017-01-26 Created: 2017-01-26 Last updated: 2019-02-27Bibliographically approved
Lindner, M., Lindner, A. & Lindgren, P. (2016). Safe tasks: run time verification of the RTFM-lang model of computation. In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016. Paper presented at 21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016. Piscataway, NJ: IEEE conference proceedings, Article ID 7733550.
Open this publication in new window or tab >>Safe tasks: run time verification of the RTFM-lang model of computation
2016 (English)In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016, Piscataway, NJ: IEEE conference proceedings, 2016, article id 7733550Conference paper, Published paper (Refereed)
Abstract [en]

Embedded systems for critical applications are typicallyspecified with requirements on predictable timing andsafety. While ensuring predictable timing, the RTFM-lang (Real-Time For the Masses) model of computation (MoC) currentlylacks memory access protection among real-time tasks. In thispaper, we discuss how to safely verify task execution given aspecification using the RTFM-MoC. Furthermore, an extensionto the RTFM-core infrastructure is outlined and tested with usecases of embedded development. We propose a method for runtime verification exploiting memory protection hardware. Forthis purpose, we introduce memory resources to the declarativelanguage RTFM-core allowing compliance checks. As a proofof concept, compiler support for model analysis and automaticgeneration of run time verification code is implemented togetherwith an isolation layer for the RTFM-kernel. With this verificationfoundation, functional run time checks as well as furtheroverhead assessments are future research questions.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE conference proceedings, 2016
Series
I E E E International Conference on Emerging Technologies and Factory Automation. Proceedings, ISSN 1946-0740
National Category
Embedded Systems
Research subject
Embedded System
Identifiers
urn:nbn:se:ltu:diva-59755 (URN)10.1109/ETFA.2016.7733550 (DOI)000389524200057 ()2-s2.0-84996551916 (Scopus ID)978-1-5090-1314-2 (ISBN)978-1-5090-1313-5 (ISBN)
Conference
21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, 6-9 Sept 2016
Available from: 2016-10-14 Created: 2016-10-14 Last updated: 2019-02-27Bibliographically approved
Organisations

Search in DiVA

Show all publications