Change search
Link to record
Permanent link

Direct link
Lindgren, Per
Publications (10 of 96) Show all publications
Lindgren, P., Dzialo, P. & Lunnikivi, H. (2023). Hardware support for Static-Priority Stack Resource Policy based scheduling. In: 2023 IEEE 32nd International Symposium on Industrial Electronics (ISIE): . Paper presented at 32nd IEEE International Symposium on Industrial Electronics (ISIE) 2023, Helsinki, Finland, June 19-21, 2023. IEEE
Open this publication in new window or tab >>Hardware support for Static-Priority Stack Resource Policy based scheduling
2023 (English)In: 2023 IEEE 32nd International Symposium on Industrial Electronics (ISIE), IEEE, 2023Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
IEEE, 2023
National Category
Computer Engineering
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-104005 (URN)10.1109/ISIE51358.2023.10228088 (DOI)2-s2.0-85172084442 (Scopus ID)
Conference
32nd IEEE International Symposium on Industrial Electronics (ISIE) 2023, Helsinki, Finland, June 19-21, 2023
Note

ISBN for host publication: 979-8-3503-9972-1

Available from: 2024-01-30 Created: 2024-01-30 Last updated: 2024-01-30Bibliographically approved
Dzialo, P., Boom, E. V. & Lindgren, P. (2023). SyncRim - A modern Simulator for Synchronous Circuits implemented in Rust. In: Jari Nurmi; Ming Shen; Peeter Ellervee; Peter Koch; Farshad Moradi (Ed.), 2023 IEEE Nordic Circuits and Systems Conference (NorCAS): . Paper presented at 2023 IEEE Nordic Circuits and Systems Conference (NorCAS), 31 October - 1 November, 2023, Aalborg, Denmark. IEEE
Open this publication in new window or tab >>SyncRim - A modern Simulator for Synchronous Circuits implemented in Rust
2023 (English)In: 2023 IEEE Nordic Circuits and Systems Conference (NorCAS) / [ed] Jari Nurmi; Ming Shen; Peeter Ellervee; Peter Koch; Farshad Moradi, IEEE, 2023Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
IEEE, 2023
National Category
Other Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-103093 (URN)10.1109/NorCAS58970.2023.10305478 (DOI)979-8-3503-3757-0 (ISBN)
Conference
2023 IEEE Nordic Circuits and Systems Conference (NorCAS), 31 October - 1 November, 2023, Aalborg, Denmark
Available from: 2023-11-29 Created: 2023-11-29 Last updated: 2023-11-29Bibliographically approved
Lindgren, P., Fitinghoff, N. & Aparicio, J. (2019). Cargo-call-stack Static Call-stack Analysis for Rust. In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN): . Paper presented at 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), 22-25 July, 2019, Helsinki-Espoo, Finland (pp. 1169-1176). IEEE
Open this publication in new window or tab >>Cargo-call-stack Static Call-stack Analysis for Rust
2019 (English)In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), IEEE, 2019, p. 1169-1176Conference paper, Published paper (Other academic)
Abstract [en]

Memory safety is instrumental to the safety and security of software systems. The Rust language stands out with a type system and underlying memory model targeting memory safety without the need for dynamic garbage collection, making Rust a viable option for embedded applications. In this paper we present an integrated tool for call-stack analysis of Rust applications. We cover both theoretical and practical challenges, their solutions and open questions. The cargo-call-stack tool is useful for analyzing Rust applications in general, and embedded Rust in particular. To the latter, we show that using the call-stack analysis we can give guarantees of total memory safety, free of assumptions on operating systems and underlying memory protection mechanisms in hardware. The feasibility of the approach is demonstrated by applying the `call-stack' tool on production code targeting a light-weight ARM Cortex-M platform.

Place, publisher, year, edition, pages
IEEE, 2019
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-78676 (URN)10.1109/INDIN41052.2019.8972088 (DOI)000529510400174 ()2-s2.0-85079059404 (Scopus ID)
Conference
2019 IEEE 17th International Conference on Industrial Informatics (INDIN), 22-25 July, 2019, Helsinki-Espoo, Finland
Note

ISBN för värdpublikation: 978-1-7281-2927-3, 978-1-7281-2928-0

Available from: 2020-04-27 Created: 2020-04-27 Last updated: 2020-06-15Bibliographically approved
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
Lindgren, P., Lindner, M. & Fitinghoff, N. (2019). Introducing Certified Compilation in Education by a Functional Language Approach. In: Peter Achten; Heather Miller (Ed.), Proceedings Seventh International Workshop on Trends in Functional Programming in Education: . Paper presented at 7th International Workshop on Trends in Functional Programming in Education (TFPIE 2018), Gothenburg, Sweden, June 14, 2018 (pp. 65-78). Open Publishing Association
Open this publication in new window or tab >>Introducing Certified Compilation in Education by a Functional Language Approach
2019 (English)In: Proceedings Seventh International Workshop on Trends in Functional Programming in Education / [ed] Peter Achten; Heather Miller, Open Publishing Association , 2019, p. 65-78Conference paper, Published paper (Refereed)
Abstract [en]

Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques through a functional language approach in an introductory course on Compiler Construction. Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language.

This paper covers the motivation, course design, tool selection, and teaching methods, together with evaluations and suggested improvements from the perspectives of both students and teachers.

Place, publisher, year, edition, pages
Open Publishing Association, 2019
Series
Electronic Proceedings in Theoretical Computer Science, E-ISSN 2075-2180 ; 295
National Category
Embedded Systems
Research subject
Dependable Communication and Computation Systems
Identifiers
urn:nbn:se:ltu:diva-73010 (URN)10.4204/EPTCS.295.5 (DOI)2-s2.0-85072205932 (Scopus ID)
Conference
7th International Workshop on Trends in Functional Programming in Education (TFPIE 2018), Gothenburg, Sweden, June 14, 2018
Available from: 2019-02-26 Created: 2019-02-26 Last updated: 2021-06-24Bibliographically approved
Lindner, M., Fitinghoff, N., Eriksson, J. & Lindgren, P. (2019). Verification of Safety Functions Implemented in Rust: a Symbolic Execution based approach. In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN): . Paper presented at 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), 22-25 July, 2019, Helsinki, Finland (pp. 432-439). IEEE
Open this publication in new window or tab >>Verification of Safety Functions Implemented in Rust: a Symbolic Execution based approach
2019 (English)In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), IEEE, 2019, p. 432-439Conference paper, Published paper (Other academic)
Abstract [en]

Symbolic execution allows us to observe and assert properties of program code executing under (partially) unknown inputs and state. In this work we present a case study demonstrating that safety functions implemented in the Rust programming language can be verified by an assertion based approach. To this end, we leverage on previous developments adopting LLVM-KLEE for symbolic execution of Rust programs.In particular we show that reliability can be ensured by proven absence of undefined behavior and that safety properties (expressed as assertions) can be ensured for all reachable paths of the underlying implementation (under symbolic inputs). Moreover, the verification (besides stating assertions) is fully automatic and can be applied without any changes made to the implementation. While assertions have the advantage of being familiar to the mainstream programmer, they lack the expressiveness of dedicated logic developed for model checking. The paper also discusses complexity issues arising from path/state explosion inherent to symbolic execution. The feasibility of the approach is demonstrated on a representative use case implementing a safety function (equality) from the PLCopen library. We obtain complete path- (466) and state- (8) coverage in under 2 seconds for the given example on an i7-7700 laptop computer.

Place, publisher, year, edition, pages
IEEE, 2019
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; Embedded Systems
Identifiers
urn:nbn:se:ltu:diva-78674 (URN)10.1109/INDIN41052.2019.8972014 (DOI)000529510400063 ()2-s2.0-85079050233 (Scopus ID)
Conference
2019 IEEE 17th International Conference on Industrial Informatics (INDIN), 22-25 July, 2019, Helsinki, Finland
Note

ISBN för värdpublikation: 978-1-7281-2927-3, 978-1-7281-2928-0

Available from: 2020-04-27 Created: 2020-04-27 Last updated: 2020-06-12Bibliographically approved
Lindgren, P., Lindner, M. & Aparicio, J. (2018). Embedded Programming adopting Functional Constructs in Rust. In: : . Paper presented at Trends in Functional Programming in Education (TFPIE 2018), Gothenburg, June 14, 2018.
Open this publication in new window or tab >>Embedded Programming adopting Functional Constructs in Rust
2018 (English)Conference paper, Oral presentation only (Refereed)
National Category
Embedded Systems
Research subject
Embedded Systems
Identifiers
urn:nbn:se:ltu:diva-73011 (URN)
Conference
Trends in Functional Programming in Education (TFPIE 2018), Gothenburg, June 14, 2018
Available from: 2019-02-26 Created: 2019-02-26 Last updated: 2021-09-01Bibliographically 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: 2021-10-14Bibliographically 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
Organisations

Search in DiVA

Show all publications