Ändra sökning
Avgränsa sökresultatet
1 - 24 av 24
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Aparicio Rivera, Jorge
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Heapless: Dynamic Data Structures without Dynamic Heap Allocator for Rust2018Ingår i: 2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), Piscataway, NJ: IEEE, 2018, s. 87-94, artikel-id 8472097Konferensbidrag (Refereegranskat)
    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.

  • 2.
    Ekman, Jonas
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Borg, Johan
    Johansson, Jonny
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    De Lauretis, Maria
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Nilsson, Joakim
    Projekt: Frekvensomriktares funktion i beredskapskritiska system2014Övrigt (Övrig (populärvetenskap, debatt, mm))
    Abstract [sv]

    Vid dödnätstart av produktionsanläggningar och drift av svaga nät eller ö-drift är frekvensomriktare som driver pumpar och fläktar kritiska komponenter. Om frekvensomriktare påverkas av störningar i nätet kan elproduktion kopplas bort och det svaga nätet eller ö-driften kollapsa. Projektet ska studera frekvensomriktare ur ett antal aspekter såsom uppbyggnad, styrning och implementering i syfte att utveckla mer robusta frekvensomriktare och implementering av dessa för att säkerställa drift av svaga nät och ö-drift och minimera ytterligare driftstörningar vid svåra påfrestningar på elnätet.

  • 3.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Eriksson, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    Response Time for IEC 61499 over Ethernet2015Ingår i: IEEE International Conference on Industrial Informatics: INDIN 2015, Cambridge, UK, July 22-24, 2015. Proceedings, Piscataway, NJ: IEEE Communications Society, 2015, s. 1206-1212, artikel-id 7281907Konferensbidrag (Refereegranskat)
    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 a message). In this paper we propose a low complexity implementation technique allowing to asses end-to-end response time of event chains spanning a networked devices. Based on a translation of IEC 61499 to RTFM-tasks and resources, the response time for each task in the system can be derived using established scheduling techniques. In this paper we develop a method to provide safe end-to-end response time taking both intra- and inter-device delivery delays into account. 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 milli-second end-to-end response times can be obtained using the proposed approach.

  • 4.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Eriksson, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    End-to-End Response Time of 61499 Distributed Applications over Switched Ethernet2017Ingår i: IEEE Transactions on Industrial Informatics, ISSN 1551-3203, E-ISSN 1941-0050, Vol. 13, nr 1, s. 287-297Artikel i tidskrift (Refereegranskat)
    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.

  • 5.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Eriksson, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    RTFM-lang static semantics for systems with mixed criticality2014Ingår i: Ada User Journal, ISSN 1381-6551, Vol. 35, nr 2, s. 128-132Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In an embedded system, functions often operate under different requirements. In the extreme, a failing safety critical function may cause collateral damage (and hence consider to be a system failure) while non critical functions affect only the quality of service. Approaches by partitioning the system's functions into sandboxes require virtualization mechanisms by the underlying platform and thus prohibit deployment to the bulk of microcontroller based systems. In this paper we discuss an alternative approach based on static semantic analysis performed directly on the system specification expressed in the form of an object oriented (00) model in the experimental language RTFM-lang. This would allow to (at compile time) to discriminate in between critical and non-critical functions, and assign these (by means of statically checkable typing rules) appropriate access rights. In particular, one can imagine dynamic memory allocations to be allowed only in non-critical functions, while on the other hand, direct interaction with the environment may be restricted to the critical parts. With respect to scheduling, a static task and resource configuration allows e.g. Stack Resource Policy (SRP) based approaches to be deployed. In this paper we discuss how this can be achieved in a mixed critical setting.

  • 6.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Fresk, Emil
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Signaler och system.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs2016Ingår i: Vol. 13, nr 1Artikel i tidskrift (Refereegranskat)
    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.

  • 7.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Fresk, Emil
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Signaler och system.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    RTFM-core: Language and Implementation2014Konferensbidrag (Refereegranskat)
    Abstract [en]

    Robustness, real-time properties and resource eciency arekey properties to embedded devices of the CPS/IoT era. Inthis paper we propose a language approach RTFM-core,and show its potential to facilitate the development processand provide highly ecient implementations amendablefor static verication. Our programming model is reactive,based on the familiar notions of concurrent tasksand (single-unit) resources. The language is kept minimalistic,capturing the static task, communication and resourcestructure of the system. Whereas C-source can be arbitrarilyembedded in the model, and/or externally referenced,the instep to mainstream development is minimal, and asmooth transition of legacy code is possible. A prototypecompiler implementation for RTFM-core is presented. Thecompiler generates C-code output that compiled togetherwith the RTFM-kernel primitives runs on bare metal. TheRTFM-kernel guarantees deadlock-lock free execution andeciently exploits the underlying interrupt hardware forstatic priority scheduling and resource management underthe Stack Resource Policy. This allows a plethora of wellknownmethods to static verication (response time analysis,stack memory analysis, etc.) to be readily applied. The proposedlanguage and supporting tool-chain is demonstratedby showing the complete process from RTFM-core sourcecode into bare metal executables for a light-weight ARMCortexM3 target.

  • 8.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Eriksson, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Vyatkin, Valeriy
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Real-Time Execution of Function Blocks for Internet of Things using the RTFM-kernel2014Ingår i: Proceedings of 2014 IEEE 19th International Conference on Emerging Technologies & Factory Automation (ETFA 2014): Barcelona, Spain, 16-19 Sept. 2014, Piscataway, NJ: IEEE Communications Society, 2014, s. 1-6, artikel-id 7005232Konferensbidrag (Refereegranskat)
    Abstract [en]

    Function Blocks provides a means to model andprogram industrial control systems. The recently acclaimed IEC61499 standard allows such system models to be partitioned andexecuted in a distributed fashion. At device level, such models aretraditionally implemented onto programmable logic controllersthat underneath have an operating system and a softwarerun-time environment which implies high resource demands.However, there is a current trend to involve small embeddedsystems (so called Internet of Things devices) integrated into suchdistributed control systems. To this end, we seek to address theoutsets for real-time execution of Function Block based designsonto light-weight controllers (MCUs) with limited resources(memory and CPU). Furthermore, we propose a mapping ofthe Function Block execution semantics onto the RTFM-kernel,and discuss opportunities for off-line (design time) analysis withrespect to response time, overall schedulability and memoryrequirements.

  • 9.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Eriksson, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Vyatkin, Valeriy
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    RTFM-4-FUN2014Ingår i: 2014 9th IEEE International Symposium on Industrial Embedded Systems (SIES 2014): Pisa, 18-20 June 2014, Piscataway, NJ: IEEE Communications Society, 2014Konferensbidrag (Refereegranskat)
    Abstract [en]

    Function Blocks provides a means to model andprogram industrial control systems. The recently acclaimed IEC61499 standard allows such system models to be partitioned andexecuted in a distributed fashion. At device level, such models aretraditionally implemented onto programmable logic controllersand industrial PCs. In this paper, we discuss work in progresson developing a mapping allowing to implement a subset of IEC61499 models onto light-weight embedded devices (MCUs). Wepropose and detail an event semantics, and its mapping to thenotions of tasks and resources for Stack Resource Policy basedanalysis and scheduling. Moreover, we show how the proposedmapping can be efficiently implemented under the RTFM-kernel.Finally we outline a prototype tool-chain and discuss related,ongoing and future work.

  • 10.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    RTFM-core: Language and Implementation2015Ingår i: 2015 IEEE 10th Conference on Industrial Electronics and Applications (ICIEA): Auckland, 15-17 June 2015, Piscataway, NJ: IEEE Communications Society, 2015, s. 990-995, artikel-id 7334252Konferensbidrag (Refereegranskat)
    Abstract [en]

    Robustness, real-time properties and resource efficiency are key properties to embedded devices of the CPS/IoT era. In this paper we propose a language approach RTFMcore, and show its potential to facilitate the development process and provide highly efficient and statically verifiable implementations. Our programming model is reactive, based on the familiar notions of concurrent tasks and (single-unit) resources. The language is kept minimalistic, capturing the static task, communication and resource structure of the system. Whereas C-source can be arbitrarily embedded in the model, and/or externally referenced, the instep to mainstream development is minimal, and a smooth transition of legacy code is possible. A prototype compiler implementation for RTFM-core is presented. The compiler generates C-code output that compiled together withtheRTFM-kernelprimitivesrunsonbaremetal.TheRTFMkernel guarantees deadlock-lock free execution and efficiently exploits the underlying interrupt hardware for static priority scheduling and resource management under the Stack Resource Policy. This allows a plethora of well-known methods to static verification (response time analysis, stack memory analysis, etc.) to be readily applied. The proposed language and supporting tool-chain is demonstrated by showing the complete process from RTFM-core source code into bare metal executables for a lightweight ARM-Cortex M3 target.

  • 11.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    Well formed Control-flow for Critical Sections in RTFM-core2015Ingår i: IEEE International Conference on Industrial Informatics: INDIN 2015, Cambridge, UK, July 22-24, 2015. Proceedings, Piscataway, NJ: IEEE Communications Society, 2015, s. 1438-1445, artikel-id 7281944Konferensbidrag (Refereegranskat)
    Abstract [en]

    The mainstream of embedded software development as of today is dominated by C programming. To aid the development, hardware abstractions, libraries, kernels and lightweight operating systems are commonplace. Such kernels and operating systems typically impose a thread based abstraction to concurrency. However, in general thread based programming is hard, plagued by hazards of race conditions and dead-locks. For this paper we take an alternative outset in terms of a language abstraction, RTFM-core, where the system is modelled directly in terms of tasks and resources. In compliance to the Stack Resource Policy (SRP) model, the language enforces (well formed) LIFO nesting of claimed resources, thus SRP based analysis and scheduling can be readily applied. For the execution onto bare-metal single core architectures, the rtfm-core compiler performs SRP analysis on the model, and render an executable that is deadlock free and (through RTFM-kernel primitives) exploits the underlying interrupt hardware for efficient scheduling. The RTFM-core language embeds C-code and links to C-object files and libraries, and is thus applicable to the mainstream of embedded development. However, while the language enforces well formed resource management, control flow in the embedded C-code may violate the LIFO nesting requirement, thus correctness is left with the programmer to ensure well formed nesting (through restricted control flow). In this paper we address this issue by lifting a subset of C into the RTFM-core language allowing arbitrary control flow at the model level. In this way well formed LIFO nesting can be enforced, and models ensured to be correct by construction. We demonstrate the feasibility trough a prototype implementation in the rtfm-core compiler. Additionally, we develop a set of running examples, and show in detail how control flow is handled at compile time and during run-time execution.

  • 12.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Vyatkin, Valeriy
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    A Real-Time Semantics for the IEC 61499 standard2015Ingår i: Proceedings of 2015 IEEE 20th International Conference on Emerging Technologies & Factory Automation (ETFA 2015): Luxembourg, 8-11 Sept. 2015, Piscataway, NJ: IEEE Communications Society, 2015, artikel-id 7301558Konferensbidrag (Refereegranskat)
    Abstract [en]

    The IEC 61499 standard provides an executable model for distributed control systems in terms of interacting function blocks. However, the current IEC 61499 standard lacks appropriate timing semantics for the specification of timing requirements, reasoning on timing properties at the model level, and for the timing verification of a specific deployment. In this paper we address this fundamental shortcoming by proposing Real-Time-4-FUN, a real-time semantics for IEC 61499. The key property is the preservation of non-determinism, allowing us to reason on (and verify) timing properties at the model level without assuming any specific scheduling policy or stipulating specific order of execution for the deployment. This provides for a clear separation of concerns, where the designer can focus on properties of the application prior to, and separately from, deployment verification. The proposed timing semantics is backwards compatible to the current standard, thus allow for reuse of existing designs. The transitional property allows timing requirements to propagate to downstream sub-systems, and can be utilized for scheduling both at device and network level. Based on a translation to RTFM-tasks and resources, IEC 61499 the models can be analyzed, compiled and executed. As a proof of concept the timing semantics has been experimentally implemented in the RTFM-core language and the accompanying (thread based) RTFM-RT run-time system.

  • 13.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David J.
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luis Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    A Formal Perspective on IEC 61499 Execution Control Chart Semantics2015Ingår i: 2015 IEEE Trustcom/BigDataSE/ISPA: Helsinki, 20-22 Aug. 2015, Piscataway, NJ: IEEE Communications Society, 2015, s. 293-300, artikel-id 7345663Konferensbidrag (Refereegranskat)
    Abstract [en]

    The IEC 61499 standard proposes an event driven execution model for distributed control applications for which an informal execution semantics is provided. Consequently, run-time implementations are not rigorously described and therefore their behavior relies on the interpretation made by the tool provider. In this paper, as a step towards a formal semantics, we focus on the Execution Control Chart semantics, which is fundamental to the dynamic behavior of Basic Function Block elements. In particular we develop a well-formedness criterion that ensures a finite number of Execution Control Chart transitions for each triggering event. We also describe the first step towards the mechanization of the well-formedness checking algorithm in the Coq proof-assistant so that, ultimately, we are able to show, once andforall,thatthisalgorithmiseffectivelycorrectwithrespectto our proposed execution semantics. The algorithm is extractable from the mechanization in a correct-by-construction way, and can be directly incorporated in certified toolchain for analysis, compilation and execution of IEC 61499 models. As a proof of concept a prototype tool RTFM-4FUN has been developed. It performs well-formedness checks on Basic Function Blocks using the extracted algorithm’s code.

  • 14.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David
    CISTER, INESC TEC, ISEP.
    Pinho, Luís Miguel
    CISTER, INESC TEC, ISEP.
    Contract Based Verification of IEC 614992017Ingår i: IEEE International Conference on Industrial Informatics (INDIN), Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017, s. 132-141, artikel-id 7819147Konferensbidrag (Refereegranskat)
    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.

  • 15.
    Lindgren, Per
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Pereira, David
    ISEP, Instituto Superior de Engenharia do Porto.
    Pinho, Luís Miguel
    ISEP, Instituto Superior de Engenharia do Porto.
    Towards Certified Compilation of RTFM-core Applications2016Ingår i: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016, Piscataway, NJ: IEEE conference proceedings, 2016, artikel-id 7733551Konferensbidrag (Refereegranskat)
    Abstract [en]

    Concurrent programming is dominated by threadbased solutions with lock based critical sections. Careful attentionhas to be paid to avoid race and deadlock conditions. Real-Timefor 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 canbe compiled to native C-code, and efficiently executed ontosingle-core platforms under the Stack Resource Policy (SRP)by the RTFM-kernel. In this paper we formally define thewell-formedness criteria for SRP based resource management,and develop a certified (formally proven) implementation ofthe corresponding compilation from nested critical sections ofthe input RTFM-core program to a resulting flat sequence ofprimitive operations and scheduling primitives. Moreover weformalise the properties for resource ceilings under SRP anddevelop a certified algorithm for their computation.The feasibility of the described approach is shown throughthe adoption of the Why3 platform, which allows the necessaryverification conditions to be automatically generated and dischargedthrough a variety of automatic external SMT-solversand interactive theorem provers. Moreover, Why3 supports theextraction of certified Ocaml code for proven implementationsin WhyML. As a proof of concept the certified extracteddevelopment is demonstrated on an example system.

  • 16.
    Lindner, Andreas
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    RTFM-RT: a threaded runtime for RTFM-core towards execution of IEC 614992015Ingår i: Proceedings of 2015 IEEE 20th International Conference on Emerging Technologies & Factory Automation (ETFA 2015): Luxembourg, 8-11 Sept. 2015, Piscataway, NJ: IEEE Communications Society, 2015, artikel-id 7301501Konferensbidrag (Refereegranskat)
    Abstract [en]

    The IEC 61449 standard provides an outset for designing and deploying distributed control systems. Recently, a mapping from IEC 61499 to the RTFM-kernel API has been presented. This allows predictable real-time execution of IEC 61499 applications on light-weight single-core platforms. However, integrating the RTFM-kernel (bare-metal runtime) into potential deployments requires developing device drivers, protocol stacks, and the like. For this presentation, we apply the mapping from IEC 61499 to the RTFM-MoC task and resource modelimplementedbytheRTFM-corelanguage.Thecompilation from RTFM-core can be targeted to both, RTFM-kernel and the introduced runtime system RTFM-RT. In this paper, we detail thegenericRTFM-RTruntimearchitecture,whichallowsRTFMcore programs to be executed on top of thread based environments. Furthermore, we discuss our implementation regarding scheduling specifics of Win32 threads (Windows) and Pthreads (Linux and Mac OS X). Using our RTFM-RT implementation for deployment,predictableIEC61499executiontogetherwithaccess to abovementioned operating system functions are achieved. For further developments, we discuss the needed scheduling options to achieve hard real-time and analysis required to eliminate deadlocks.

  • 17.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Robust industrial automation software: outsets for non-determinism and real-time execution2016Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    Studies about the industrial standard IEC 61499 and its relation to the RTFM Model of Computation represent the basis of this thesis. An overview of industrial automation software in general and in the scope of Svenska Kraftnät introduces the subject of software related issues. The thesis focuses on selected properties, which are important for software development to improve the robustness of industrial automation software. Among others, timing is essential due to its importance in real-time applications. An example case of the nuclear power plant Forsmark in Sweden illustrates problems correlated with timing issues and makes the lack of an overall system modelling (including timing) evident. A review of the relevant industrial standards for software development in industrial applications provides a background for various aspects of software compliance to safety requirements. Special attention lies on the standards IEC 61131 and IEC 61499 for industrial software development and their programming and execution model. The presented RTFM framework defines a concurrent model of execution based on tasks and resources together with a timing semantics that was designed from the outset for the development of embedded real-time systems. It can serve as a scheduling and resource management for the run-time environments of industrial applications, while addressing the aforementioned issues. Mappings from the functional layer (IEC 61499 function block networks) and safety layer (PLCopen safety function blocks) to RTFM show the applicability and possibility of using IEC 61499 as an overall, distributed, and hierarchical model. A discussion on options for future work presents choices to pursue the second half of the PhD studies. Formal methods for program specification and verification open up an interesting path to further increase the robustness of industrial automation software.

  • 18.
    Lindner, Marcus
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    !secure(system) <=?=> !safe(system): On Security and Safety of Industrial Software Systems2019Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    The focus of our research work is on readily accessible, embedded, real-time development with concurrency support. To this end, we develop the Real-Time For the Masses (RTFM) programming framework with a model of computation based on tasks and resources and that stipulates a timing semantics. Typically, hard real-time requirements are a characteristic of safety-critical applications. In contrast to runtime verification, such applications primarily require static assurances concerning safety and security attributes. This thesis discusses the building blocks for a statically analyzable programming paradigm for embedded real-time applications and its implementation. Svenska kraftnät funded the research presented in this thesis and set the scope to industrial automation. Consequently, we also investigate the applicability of our RTFM framework for scheduling and resource management for the runtime environments of industrial applications. We start by reviewing relevant and well-established industry standards to build background knowledge of the state-of-the-art safety and security requirements in software development. Special attention is placed on the IEC 61131 and IEC 61499 standards for industrial software development and their programming and execution model. We show the feasibility of using IEC 61499 as a holistic, distributed, and hierarchical model with mappings from the functional layer (IEC 61499 function block networks) and safety layer (PLCopen safety function blocks) to RTFM. We also demonstrate that our Rust-based RTFM implementation enables static verification for a myriad of safety and security attributes. Moreover, our investigations reveal a mutual dependency of safety and security in the context of software systems. For this reason, we believe and argue that safety and security cannot be considered independent during the design and implementation of safety-critical applications. Upon closer examination, we even conclude that safety and security are equivalent.

     

  • 19.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Aparicio, Jorge
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Concurrent Reactive Objects in Rust Secure by Construction2019Ingår i: Ada User Journal, ISSN 1381-6551, Vol. 40, nr 1Artikel i tidskrift (Refereegranskat)
    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.

  • 20.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Aparicio, Jorge
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    No Panic! Verification of Rust Programs by Symbolic Execution2018Konferensbidrag (Refereegranskat)
    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.

  • 21.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Aparicio, Jorge
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Tjäder, Henrik
    Luleå tekniska universitet, Verksamhetsstöd.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB. Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Eriksson, Johan
    Grepit AB, Lulea.
    Hardware-in-the-loop based WCET analysis with KLEE2018Ingår i: 2018 IEEE 23RD INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), Piscataway, NJ: IEEE, 2018, s. 345-352Konferensbidrag (Refereegranskat)
    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.

  • 22.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    RTFM-core: Course in Compiler Construction2014Ingår i: Proceedings of the WESE'14: Workshop on Embedded and Cyber-Physical Systems Education, New York: ACM Digital Library, 2014, artikel-id 4Konferensbidrag (Refereegranskat)
    Abstract [en]

    The course in Compiler Construction is part of the ComputerScience second cycle curriculum at Lulea Universityof Technology (LTU). Starting this year, the course is nowto be given by the Embedded Systems group at LTU. Thispaper outlines the course syllabus, and its relation to CPS/IoT and embedded systems in general. In particular, thecourse will now introduce domain specic language designwith the outset from the RTFM-core language. Studentswill be exposed to design choices for the language, spanningfrom programming model, compiler design issues, backendtools and even run-time environments. The intention is togive a holistic perspective, and motivate the use of compilationtechniques towards robust, ecient and veriable (embedded)software. Of course, developing basic skills will notbe overlooked, and as part of the laboratory assignments,students will extend the minimalistic Object Oriented languageRTFM-cOOre and develop the compiler accordinglytargeting the RTFM-core language as an intermediate representation.As the RTFM-core/-cOOre compilers are implementedunder OCaml/Menhir, the students will be exposedto the advantages of functional languages in the contextof compiler construction. However, for their own developmentthey may choose alternative design tools and languages(such as ANTLR/Java). This will give us the opportunityto review and correlate achievements and eciencyto the choice of tools and languages and be an outset forfuture course development.

  • 23.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    RTFM-core: course in compiler construction2016Ingår i: The SIGBED Review, ISSN 1551-3688, Vol. 14, nr 1, s. 29-36Artikel i tidskrift (Refereegranskat)
    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.

  • 24.
    Lindner, Marcus
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindner, Andreas
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Lindgren, Per
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, EISLAB.
    Safe tasks: run time verification of the RTFM-lang model of computation2016Ingår i: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA): Berlin, 6-9 Sept. 2016, Piscataway, NJ: IEEE conference proceedings, 2016, artikel-id 7733550Konferensbidrag (Refereegranskat)
    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.

1 - 24 av 24
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf