liu.seSearch for publications in DiVA
Change search
Refine search result
123456 51 - 100 of 265
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 51.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Formal Coverification of Embedded Systems using Model Checking2000In: 26th Euromicro Conference Digital Systems Design,2000, Maastricht, The Netherlands: IEEE Computer Society Press , 2000, p. 106-113 vol.1Conference paper (Refereed)
    Abstract [en]

    The complexity of embedded systems is increasing rapidly. In consequence, new verification techniques that overcome the limitations of traditional methods and are suitable for hardware/software systems are needed. In this paper we introduce a computational model for embedded systems based on Petri nets, called PRES. We present an approach to coverification of both the hardware and software parts of an embedded system represented by PRES. We use symbolic model checking to prove the correctness of such systems, specifying properties in CTL and verifying whether they are satisfied. This coverification method permits to reason formally about design properties as well as timing requirements. A medical monitoring system illustrates the feasibility of our approach on practical applications.

  • 52.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    From Haskell to PRES+ Basic Translation Procedures2001Report (Other academic)
    Abstract [en]

    We define in this report some basic procedures to translate Haskell descriptions (based on a library of Skeletons) into PRES+ models. In this way, a system initially described in Haskell, may be transformed into a representation that might be formally verified. Thus the representa-tion of the system is verified using formal methods by model-checking the model against a set of required properties expressed by temporal logics. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous elec-tronic systems.

  • 53.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Hierarchical Modeling and Verification of Embedded Systems2001In: Euromicro Symposium on Digital Systems Design,2001, Warsaw, Poland: IEEE Computer Society Press , 2001, p. 63-Conference paper (Refereed)
    Abstract [en]

    In order to represent efficiently large systems, a mechanism for hierarchical composition is needed so that the model may be constructed in a structured manner and composed of simpler units easily comprehensible by the designer at each description level. In this paper we formally define the notion of hierarchy for a Petri net based representation used for modeling embedded systems. We show how small parts of a large system may be transformed by using the concept of hierarchy and the advantages of a transformational approach in the verification of embedded systems. A real-life example illustrates the feasibility of our approach on practical applications.

  • 54.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Hierarchies for the Modeling and Verification of Embedded Systems2001Report (Other academic)
    Abstract [en]

    A flat representation of a realistic embedded system can be too big and complex to handle and understand. In order to represent efficiently large systems, a mechanism for hierarchical com-position is needed so that the model may be constructed in a structured manner and composed of simpler units easily comprehensible by the designer at each description level. In this report we formally define the notion of hierarchy for a Petri net based representation used for mode-ling embedded systems. We show how small parts of a large system may be transformed by using the concept of hierarchy as well as the advantages of a transformational approach in the verification of embedded systems. A real-life example illustrates the feasibility of our approach on practical applications. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous electronic systems.

  • 55.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Modeling and formal verification of embedded systems based on a Petri net representation2003In: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165, Vol. 49, no 12-15, p. 571-598Article in journal (Refereed)
    Abstract [en]

    In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications. © 2003 Elsevier B.V. All rights reserved.

  • 56.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Modeling and Verification of Embedded Systems using Petri Net based Methods: Application to an Industrial Case2001Report (Other academic)
    Abstract [en]

    Embedded systems are becoming increasingly common in objects that we use in our everyday life. Embedded systems are typically characterized by their dedicated function and real-time behavior. Many of them must fulfill strict requirements in terms of reliability and correctness. Designing systems with such features, combined with high levels of complexity and tight time-to-market constraints, is a challenging task. In order to devise systems with such features, a formal design methodology is necessary to carry out systematically the different tasks along the design flow. The SAVE project aims at the development of a formal approach to specification, implementation, and verification of heterogeneous electronic systems. We have developed techniques for modeling and verifying embedded systems. This document reports the main results that have been obtained within the frame of SAVE in the fields of modeling and verification. An industrial system is used as study case in order to demonstrate the feasibility of the approach on practical applications.

  • 57.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Quasi-Static Assignment of Voltages and Optional Cycles for Maximizing Rewards in Real-Time Systems with Energy Constraints2005In: 42nd Design Automation Conference,2005, Anaheim, CA, USA: IEEE Computer Society Press , 2005, p. 889-Conference paper (Refereed)
    Abstract [en]

    There exist real-time systems for which it is possible to trade off precision for timeliness. In these cases, a function assigns reward to the application depending on the amount of computation allotted to it. At the same time, many such applications run on battery-powered devices with stringent energy constraints. This paper addresses the problem of maximizing rewards subject to time and energy constraints. We propose a quasi-static approach where the problem is solved in two steps: first, at design-time, a number of solutions are computed and stored (off-line phase); second, one of the precomputed solutions is selected at run-time based on actual values of time and energy (on-line phase). Thus our approach is able to exploit, with low on-line overhead, the dynamic slack caused by tasks executing less number of cycles than in the worst case. We conduct numerous experiments in order to show the advantages of our approach.

  • 58.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks2003Report (Other academic)
    Abstract [en]

    We address in this report the problem of scheduling for multiprocessor real-time systems comprised of hard and soft tasks. We use utility functions associated to soft tasks that capture their relative importance and how the quality of results is influenced when a soft deadline is missed. The problem is thus finding a task execution order that maximizes the total utility and guarantees meeting the hard deadlines. We consider time intervals rather than fixed execution times for tasks. On the one hand, a single static schedule computed off-line is too pessimistic. On the other hand, a purely on-line approach, which computes a new schedule every time a task completes considering the actual conditions, incurs an overhead that is unacceptable due to the high complexity of the problem. We propose a quasi-static solution where a number of schedules are computed at design-time, letting only for run-time the selection of a particular schedule based on the actual execution times. We propose an exact algorithm as well as heuristics that tackle the time and memory complexity of the problem. We evaluate our approach through synthetic examples and a realistic application.

  • 59.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks2005In: 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications RTCSA05,2005, Hong Kong: IEEE Computer Society Press , 2005, p. 422-Conference paper (Refereed)
    Abstract [en]

    We address in this paper the problem of scheduling for multiprocessor real-time systems with hard and soft tasks. Utility functions are associated to soft tasks to capture their relative importance and how the quality of results is affected when a soft deadline is missed. The problem is to find a task execution order that maximizes the total utility and guarantees the hard deadlines. In order to account for actual execution times, we consider time intervals for tasks rather than fixed execution times. A single static schedule computed off-line is pessimistic, while a purely on-line approach, which computes a new schedule every time a task completes, incurs an unacceptable overhead. We propose therefore a quasi-static solution where a number of schedules are computed at design time, leaving for run-time only the selection of a particular schedule, based on the actual execution times. We propose an exact algorithm as well as heuristics that tackle the time and memory complexity of the problem. We evaluate our approach through synthetic examples and a realistic application.

  • 60.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks2003Report (Other academic)
    Abstract [en]

    This report addresses the problem of scheduling for real-time systems that include both hard and soft tasks. In order to capture the relative importance of soft tasks and how the quality of results is affected when missing a soft deadline, we use utility functions associated to soft tasks. Thus the aim is to find the execution order of tasks that makes the total utility maximum and guarantees hard deadlines. We consider intervals rather than fixed execution times for tasks. Since a purely off-line solution is too pessimistic and a purely on-line approach incurs an unacceptable overhead due to the high complexity of the problem, we propose a quasi-static approach where a number of schedules are prepared at design-time and the decision of which of them to follow is taken at run-time based on the actual execution times. We propose an exact algorithm as well as different heuristics for the problem addressed in this report.

  • 61.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks2004In: Design, Automation and Test in Europe DATE 2004,2004, Paris, France: IEEE Computer Society Press , 2004, p. 1176-Conference paper (Refereed)
    Abstract [en]

    This paper addresses the problem of scheduling for real-time systems that include both hard and soft tasks. The relative importance of soft tasks and how the quality of results is affected when missing a soft deadline are captured by utility functions associated to soft tasks. Thus the aim is to find the execution order of tasks that makes the total utility maximum and guarantees hard deadlines. We consider time intervals rather than fixed execution times for tasks. Since a purely off-line solution is too pessimistic and a purely on-line approach incurs an unacceptable overhead due to the high complexity of the problem, we propose a quasi-static approach where a number of schedules are prepared at design-time and the decision of which of them to follow is taken at run-time based on the actual execution times. We propose an exact algorithm as well as different heuristics for the problem addressed in this paper.

  • 62.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks2003Report (Other academic)
    Abstract [en]

    In this report we address the problem of static scheduling of real-time systems that include both hard and soft tasks. We consider systems in which both hard and soft tasks are periodic, and our analysis take into account the data dependencies among tasks. In order to capture the relative importance of soft tasks and how the quality of results is affected when missing a soft deadline, we use utility functions associated to soft tasks. Thus our objective is to find a schedule that maximizes the total utility and at the same time guarantees hard deadlines. We use the expected duration of tasks for evaluating utility functions whereas we use the maximum duration of tasks for ensuring that hard deadlines are always met. We show that the problem we study in this report is NP-complete and we present an algorithm that finds the optimal schedule as well as different heuristics that find near-optimal solutions at reasonable computational cost.

  • 63.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks2004In: The IEEE International Workshop on Electronic Design, Test and Applications DELTA 2004,2004, 2004, p. 115-120Conference paper (Refereed)
    Abstract [en]

    In this paper we address the problem of static scheduling of real-time systems that include both hard and soft tasks. We consider that hard as well as soft tasks are periodic and that there exist data dependencies among tasks. In order to capture the relative importance of soft tasks and how the quality of results is affected when missing a soft deadline, we use utility functions associated to soft tasks. Thus our objective is to find an execution order for tasks that maximizes the total utility and at the same time guarantees hard deadlines. We use the expected duration of tasks for evaluating utility functions whereas we use the maximum duration of tasks for ensuring that hard deadlines are always met. We present an algorithm for finding the optimal schedule and also different heuristics that find near-optimal solutions at reasonable computational cost. The proposed algorithms are evaluated using a large number of synthetic examples.

  • 64.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Verification Methodology for Heterogeneous Hardware/Software Systems2000Report (Other academic)
    Abstract [en]

    Modern electronic systems are constituted by heterogeneous elements, e.g. hardware/software, and are typically embedded. The complexity of this kind of systems is such, that traditional validation techniques, like simulation and testing, are not enough to verify the correctness of these systems. In consequence, new formal verification techniques that overcome the limitations of traditional validation methods and are suitable for hardware/software systems are needed. Formal methods require the system to be represented by a formal computational model with clear semantics. We present a Petri net based representation, called PRES, which is able to capture information relevant to embedded systems. This report also explores an approach to formal verification of embedded systems in which the underlying representation is PRES. We use symbolic model checking to prove the correctness of such systems, specifying properties in CTL and verifying whether they hold under all possible situations. This coverification method permits to reason formally about design properties as well as timing requirements. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous electronic systems.

  • 65.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Verification of Embedded Systems using a Petri Net based Representation2000In: 13th International Symposium on System Synthesis ISSS 2000,2000, Madrid, Spain: IEEE Computer Society Press , 2000, p. 149-155Conference paper (Refereed)
    Abstract [en]

    The ever increasing complexity of embedded systems consisting of hardware and software components poses a challenge in verifying their correctness. New verification methods that overcome the limitations of traditional techniques and, at the same time, are suitable for hardware/software systems are needed. In this work we formally define the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. We introduce an approach to formal verification of such systems: we make use of model checking to prove the correctness of embedded systems by determining the truth of CTL and TCTL formulas that specify required properties with respect to a PRES+ model. An ATM server illustrates the feasibility of our approach on practical applications.

  • 66.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Verification of Heterogeneous Electronic Systems using Model Checking2000Report (Other academic)
    Abstract [en]

    The ever increasing complexity of heterogeneous electronic systems consisting of hardware and software components poses a challenge in verifying their correctness. The complexity of this kind of systems is such, that traditional validation methods, like simulation and testing, are not enough to verify their correctness. In consequence, new verification methods that over-come the limitations of traditional techniques and, at the same time, are suitable for heteroge-neous hardware/software systems are needed. In this report we formally define the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. We introduce an approach to formal verification of heterogeneous electronic systems: we make use of model checking to prove the correctness of such systems by determining the truth of CTL and TCTL formulas that specify required properties with respect to a PRES+ model. Thus verification with timing properties is possible. An ATM server illustrates the feasibility of this approach on practical applications. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous electronic systems.

  • 67.
    Cortes, Luis-Alejandro
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata2002In: 8th International Conference on Real-Time Computing Systems and Applications RTCSA 2002,2002, 2002, p. 191-199Conference paper (Refereed)
    Abstract [en]

    There is a lack of new verification methods that overcome the limitations of traditional validation techniques and are, at the same time, suitable for real-time embedded systems. This paper presents an approach to formal verification of real-time embedded systems modeled in a timed Petri net representation. We translate the Petri net model into timed automata and use model checking to prove whether certain properties hold with respect to the system model. We propose two strategies to improve the efficiency of verification. First, we apply correctness-preserving transformations to the system model in order to obtain a simpler, yet semantically equivalent, one. Second, we exploit the structure of the system model by extracting its the sequential behavior. Experimental results demonstrate significant improvements in the efficiency of verification.

  • 68.
    Ejlali, Alireza
    et al.
    Sharif University of Technology.
    Al-Hashimi, Bashir
    University of Southampton.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    A Standby-Sparing Technique with Low Energy-Overhead for Fault-Tolerant Hard Real-Time Systems2009In: Intl. Conference on Hardware-Software Co-Design and System Synthesis (CODES/ISSS), Grenoble, France, October 11-16, 2009 (best paper award)., 2009, p. 193-202Conference paper (Refereed)
    Abstract [en]

    Time redundancy (rollback-recovery) and hardware redundancy are commonly used in real-time systems to achieve fault tolerance. From an energy consumption point of view, time redundancy is generally more preferable than hardware redundancy. However, hard real-time systems often use hardware redundancy to meet high reliability requirements of safety-critical applications. In this paper we propose a hardware-redundancy technique with low energy-overhead for hard real-time systems. The proposed technique is based on standby-sparing, where the system is composed of a primary unit and a spare. Through analytical models, we have developed an online energy-management method which uses a slack reclamation scheme to reduce the energy consumption of both the primary and spare units. In this method, dynamic voltage scaling (DVS) is used for the primary unit and dynamic power management (DPM) is used for the spare. We conducted several experiments to compare the proposed system with a fault-tolerant real-time system which uses time redundancy for fault tolerance and DVS with slack reclamation for low energy consumption. The results show that for relaxed time constraints, the proposed system provides up to 24% energy saving as compared to the time-redundancy system. For tight deadlines when the time-redundancy system can tolerate no faults, the proposed system preserves its fault-tolerance but with about 32% more energy consumption.

  • 69.
    Ejlali, Alireza
    et al.
    Sharif University of Technology, Theran, Iran.
    Al-Hashimi, Bashir M
    University of Southampton.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Low-Energy Standby-Sparing for Hard Real-Time Systems2012In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, ISSN 0278-0070, E-ISSN 1937-4151, Vol. 31, no 3, p. 329-342Article in journal (Refereed)
    Abstract [en]

    Time-redundancy techniques are commonly used in real-time systems to achieve fault tolerance without incurring high energy overhead. However, reliability requirements of hard real-time systems that are used in safety-critical applications are so stringent that time-redundancy techniques are sometimes unable to achieve them. Standby sparing as a hardware-redundancy technique can be used to meet high reliability requirements of safety-critical applications. However, conventional standby-sparing techniques are not suitable for low-energy hard real-time systems as they either impose considerable energy overheads or are not proper for hard timing constraints. In this paper we provide a technique to use standby sparing for hard real-time systems with limited energy budgets. The principal contribution of this paper is an online energy-management technique which is specifically developed for standby-sparing systems that are used in hard real-time applications. This technique operates at runtime and exploits dynamic slacks to reduce the energy consumption while guaranteeing hard deadlines. We compared the low-energy standby-sparing (LESS) system with a low-energy time-redundancy system (from a previous work). The results show that for relaxed time constraints, the LESS system is more reliable and provides about 26% energy saving as compared to the time-redundancy system. For tight deadlines when the time-redundancy system is not sufficiently reliable (for safety-critical application), the LESS system preserves its reliability but with about 49% more energy consumption.

  • 70.
    Eles, Petru Ion
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Doboli, A.
    IEEE, Department of Electrical and Computer Engineering and Computer Science, University of Cincinnati, Cincinnati, OH 45221, United States.
    Pop, Paul
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Scheduling with bus access optimization for distributed embedded systems2000In: IEEE Transactions on Very Large Scale Integration (vlsi) Systems, ISSN 1063-8210, E-ISSN 1557-9999, Vol. 8, no 5, p. 472-491Article in journal (Refereed)
    Abstract [en]

    In this paper, we concentrate on aspects related to the synthesis of distributed embedded systems consisting of programmable processors and application-specific hardware components. The approach is based on an abstract graph representation that captures, at process level, both dataflow and the flow of control. Our goal is to derive a worst case delay by which the system completes execution, such that this delay is as small as possible, to generate a logically and temporally deterministic schedule, and to optimize parameters of the communication protocol such that this delay is guaranteed. We have further investigated the impact of particular communication infrastructures and protocols on the overall performance and, specially, how the requirements of such an infrastructure have to be considered for process and communication scheduling. Not only do particularities of the underlying architecture have to be considered during scheduling but also the parameters of the communication protocol should be adapted to fit the particular embedded application. The optimization algorithm, which implies both process scheduling and optimization of the parameters related to the communication protocol, generates an efficient bus access scheme as well as the schedule tables for activation of processes and communications.

  • 71.
    Eles, Petru Ion
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Izosimov, Viacheslav
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Pop, Paul
    Dept. Informatics and Mathematical Modelling Technical University of Denmark.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Synthesis of Fault-Tolerant Embedded Systems2008In: Design, Automation and Test in Europe, 2008., Munich, Germany: IEEE , 2008, p. 960-965Conference paper (Refereed)
    Abstract [en]

    This work addresses the issue of design optimization for fault-tolerant hard real-time systems. In particular, our focus is on the handling of transient faults using both checkpointing with rollback recovery and active replication. Fault tolerant schedules are generated based on a conditional process graph representation. The formulated system synthesis approaches decide the assignment of fault-tolerance policies to processes, the optimal placement of checkpoints and the mapping of processes to processors, such that multiple transient faults are tolerated, transparency requirements are considered, and the timing constraints of the application are satisfied.

  • 72.
    Eles, Petru Ion
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jantsch, A.
    Department of Electronic, Communication, and Software Systems, School for Information and Communication Technology, Royal Institute of Technology, Stockholm SE-164 40, Sweden.
    IEEE Transactions on Very Large Scale Integration (VLSI) Systems: Guest editorial2006In: IEEE Transactions on Very Large Scale Integration (vlsi) Systems, ISSN 1063-8210, E-ISSN 1557-9999, Vol. 14, no 8, p. 789-790p. 789-790Article in journal (Other academic)
  • 73.
    Eles, Petru Ion
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jantsch, A.
    Royal Institute of Technology, Department of Electronic, Communication, and Software Systems, School for Information and Communication Technology, Stockholm SE-164 40, Sweden.
    IEEE Transactions on Very Large Scale Integration (VLSI) Systems: Guest Editorial2006In: IEEE Transactions on Very Large Scale Integration (vlsi) Systems, ISSN 1063-8210, E-ISSN 1557-9999, Vol. 14, no 7, p. 665-666p. 665-666Article in journal (Other academic)
  • 74.
    Eles, Petru Ion
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jervan, Gert
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Mohamed, Abdil
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Report on Early DfT Support2002Report (Other academic)
    Abstract [en]

    The main goal of workpackage 3 of the COTEST project was assessment of the feasibility and evaluation of test-oriented system modifications. This report introduces some possible techniques and discuss their effectiveness for early DfT support.

  • 75.
    Eles, Petru Ion
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Kuchcinski, Krzysztof
    Dept. of Computer Science Lund University.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Doboli, Alex
    Dept. of Electrical and Computer Engineering State University of New York at Stony Brook.
    Pop, Paul
    Dept. Informatics and Mathematical Modelling Technical University of Denmark.
    Scheduling of Conditional Process Graphs for the Synthesis of Embedded Systems2008In: Design, Automation, and Test in Europe: The Most Influential Papers of 10 Years DATE, Dordrecht, The Netherlands: Springer , 2008, 1, p. 15-29Chapter in book (Other academic)
    Abstract [en]

    We present an approach to process scheduling based on an abstract graph representation which captures both data-flow and the flow of control. Target architectures consist of several processors, ASICs and shared busses. We have developed a heuristic which generates a schedule table so that the worst case delay is minimized. Several experiments demonstrate the efficiency of the approach.

  • 76.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Safety Verification of Phaser Programs2017In: PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), IEEE , 2017, p. 68-75Conference paper (Refereed)
    Abstract [en]

    We address the problem of statically checking control state reachability (as in possibility of assertion violations, race conditions or runtime errors) and plain reachability (as in deadlock-freedom) of phaser programs. Phasers are a modern non-trivial synchronization construct that supports dynamic parallelism with runtime registration and deregistration of spawned tasks. They allow for collective and point-to-point synchronizations. For instance, phasers can enforce barriers or producer-consumer synchronization schemes among all or subsets of the running tasks. Implementations are found in modern languages such as Habanero Java. Phasers essentially associate phases to individual tasks and use their runtime values to restrict possible concurrent executions. Unbounded phases may result in infinite transition systems even in the case of programs only creating finite numbers of tasks and phasers. We introduce an exact gap-order based procedure that always terminates when checking control reachability for programs generating bounded numbers of coexisting tasks and phasers. We also show verifying plain reachability is undecidable even for programs generating few tasks and phasers. We then explain how to turn our procedure into a sound analysis for checking plain reachability (including deadlock freedom). We report on preliminary experiments with our open source tool.

  • 77.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Abstracting and Counting Synchronizing Processes2014Report (Other academic)
    Abstract [en]

    We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables refering to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes. 

  • 78.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Counting dynamically synchronizing processes2016In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, p. 517-534Article in journal (Refereed)
    Abstract [en]

    We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

  • 79.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Lazy Constrained Monotonic Abstraction2016In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings / [ed] Barbara Jobstmann; K. Rustan M. Leino, Springer Berlin/Heidelberg, 2016, Vol. 9583, p. 147-165Conference paper (Refereed)
    Abstract [en]

    We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.

  • 80.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Henrio, Ludovic
    Univ Lyon, EnsL, UCBL, CNRS, Inria, LIPLyon Cedex 07France.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    On Reachability in Parameterized Phaser Programs2019Conference paper (Refereed)
    Abstract [en]

    We address the problem of statically checking safety properties (such as assertions or deadlocks) for parameterized phaser programs. Phasers embody a non-trivial and modern synchronization construct used to orchestrate executions of parallel tasks. This generic construct supports dynamic parallelism with runtime registrations and deregistrations of spawned tasks. It generalizes many synchronization patterns such as collective and point-to-point schemes. For instance, phasers can enforce barriers or producer-consumer synchronization patterns among all or subsets of the running tasks. We consider in this work programs that may generate arbitrarily many tasks and phasers. We propose an exact procedure that is guaranteed to terminate even in the presence of unbounded phases and arbitrarily many spawned tasks. In addition, we prove undecidability results for several problems on which our procedure cannot be guaranteed to terminate.

  • 81.
    Ganjei, Zeinab
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Ion Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
    Abstracting and Counting Synchronizing Processes2015In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015., Springer, 2015, p. 227-244Conference paper (Refereed)
    Abstract [en]

    We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables referring to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes.

  • 82.
    Goloubeva, Olga
    et al.
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Reorda, Matteo Sonza
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Violante, Massimo
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jervan, Gert
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Final Report on Project Results2002Report (Other academic)
    Abstract [en]

    The COTEST project aimed at assessing whether it is feasible and effective to take test issues into account early in the circuit design process, when a behavioral description of the circuit is available, only. The project focused on two main problems: generation of test sequences starting from behavioral descriptions and modification of behavioral descriptions to increase testability (Design for Testability). Due to the critical nature of this assessment project, it is extremely important to obtain as much feedback about the results as possible. The results have been discussed on meetings with industry, academic partners and in the framework of several other Community projects. Several scientific papers have been published or submitted for publication. In this report the current dissemination status and future dissemination plans of both partners will be given.

  • 83.
    Goloubeva, Olga
    et al.
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Reorda, Matteo Sonza
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Violante, Massimo
    Dipartimento di Automatica e Informatica Politecnico di Torino.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jervan, Gert
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Report on Dissemination Plan2002Report (Other academic)
    Abstract [en]

    The COTEST project aimed at assessing whether it is feasible and effective to take test issues into account early in the circuit design process, when a behavioral description of the circuit is available, only. The project focused on two main problems: generation of test sequences starting from behavioral descriptions and modification of behavioral descriptions to increase testability (Design for Testability). Due to the critical nature of this assessment project, it is extremely important to obtain as much feedback about the results as possible. The results have been discussed on meetings with industry, academic partners and in the framework of several other Community projects. Several scientific papers have been published or submitted for publication. In this report the current dissemination status and future dissemination plans of both partners will be given.

  • 84.
    Ha, Soonhoi
    et al.
    Seoul Natl Univ, South Korea.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    2018 Embedded Systems Week (ESWEEK) in Torino2019In: IEEE design & test, ISSN 2168-2356, E-ISSN 2168-2364, Vol. 36, no 1, p. 68-69Article in journal (Other academic)
    Abstract [en]

    n/a

  • 85.
    Ha, Soonhoi
    et al.
    Seoul Natl Univ, South Korea.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Editorial2018In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, ISSN 0278-0070, E-ISSN 1937-4151, Vol. 37, no 11, p. 2187-2187Article in journal (Other academic)
    Abstract [en]

    n/a

  • 86.
    Ha, Soonhoi
    et al.
    Seoul National University, South Korea.
    Teich, Jürgen
    Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany.
    Haubelt, Christian
    Universität Rostock, Germany.
    Glaß, Michael
    Ulm University, Germany.
    Mitra, Tulika
    National University of Singapore, Singapore.
    Dömer, Rainer
    University of California, Irvine, USA.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Shrivastava, Aviral
    Arizona State University, USA.
    Gerstlauer, Andreas
    The University of Texas at Austin, USA.
    Bhattacharyya, Shuvra S.
    University of Maryland, USA; Tampere University of Technology, Finland.
    Introduction to Hardware/Software Codesign2017In: Handbook of Hardware/Software Codesign / [ed] Soonhoi Ha, Jürgen Teich, Springer Netherlands, 2017Chapter in book (Refereed)
    Abstract [en]

    Hardware/Software Codesign (HSCD) is an integral part of modern Electronic System Level (ESL) design flows. This chapter will review important aspects of hardware/software codesign flows, summarize the historical evolution of codesign techniques, and subsequently summarize each of its major branches of research and achievements that later will be presented in detail by different parts of this Handbook of Hardware/Software Codesign.

  • 87.
    He, Zhiyuan
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jervan, Gert
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Power-Constrained Hybrid BIST Test Scheduling in an Abort-on-First-Fail Test Environment2005In: 8th Euromicro Conference on Digital System Design DSD2005,2005, Porto, Portugal: IEEE Computer Society Press , 2005, p. 83-Conference paper (Refereed)
    Abstract [en]

    This paper presents a method for power-constrained system-on-chip test scheduling in an abort-on-first-fail environment where the test is terminated as soon as a fault is detected. We employ the defect probabilities of individual cores to guide the scheduling, such that the expected total test time is minimized and the peak power constraint is satisfied. Based on a hybrid BIST architecture where a combination of deterministic and pseudorandom test sequences is used, the power-constrained test scheduling problem can be formulated as an extension of the two-dimensional rectangular packing problem and a heuristic has been proposed to calculate the near optimal order of different test sequences. The method is also generalized for both test-per-clock and test-per-scan approaches. Experimental results have shown that the proposed heuristic is efficient to find a near optimal test schedule with a low computation overhead.

  • 88.
    He, Zhiyuan
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Jervan, Gert
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Hybrid BIST Test Scheduling Based on Defect Probabilities2004In: 2004 IEEE Asian Test Symposium ATS 2004,2004, Kenting, Taiwan: IEEE Computer Society Press , 2004, p. 230-Conference paper (Refereed)
    Abstract [en]

    This paper describes a heuristic for system-on-chip test scheduling in an abort-on-fail context, where the test is terminated as soon as a defect is detected. We consider an hybrid BIST architecture, where a test set is assembled from pseudorandom and deterministic test patterns. We take into account defect probabilities of individual cores in order to schedule the tests so that the expected total test time in the abort-on fail environment is minimized. Different from previous approaches, our hybrid BIST based approach enables us not only to schedule the tests but also to modify the internal test composition, the order and ratio of pseudorandom and deterministic test patterns, in order to reduce the expected total test time. Experimental results have shown the efficiency of the proposed heuristic to find good quality solutions with low computational overhead.

  • 89.
    He, Zhiyuan
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    A heuristic for thermal-safe SoC test scheduling2007In: IEEE International Test Conference, 2007, IEEE , 2007, p. 116-125Conference paper (Refereed)
    Abstract [en]

    High temperature has become a technological barrier to the testing of high performance systems-on-chip, especially when deep submicron technologies are employed. In order to reduce test time while keeping the temperature of the cores under test within a safe range, thermal-aware test scheduling techniques are required. In this paper, we address the test time minimization problem as how to generate the shortest test schedule such that the temperature limits of individual cores and the limit on the test-bus bandwidth are satisfied. In order to avoid overheating during the test, we partition test sets into shorter test sub-sequences and add cooling periods in between, such that continuously applying a test sub-sequence will not drive the core temperature going beyond the limit. Further more, based on the test partitioning scheme, we interleave the test sub-sequences from different test sets in such a manner that a cooling period reserved for one core is utilized for the test transportation and application of another core. We have proposed a heuristic to minimize the test application time by exploring alternative test partitioning and interleaving schemes with variable length of test sub-sequences and cooling periods. Experimental results have shown the efficiency of the proposed heuristic.

  • 90.
    He, Zhiyuan
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Power Constrained and Defect-Probability Driven SoC Test Scheduling with Test Set Partitioning2006In: Design Automation and Test in Europe Conference DATE 2006,2006, Munich, Germany: IEEE Computer Society Press , 2006, p. 291-Conference paper (Refereed)
    Abstract [en]

    This paper presents a test scheduling approach for system-on-chip production tests with peak-power constraints. An abort-on-first-fail test approach is assumed, whereby the test is terminated as soon as the first fault is detected. Defect probabilities of individual cores are used to guide the test scheduling and the peak-power constraint is considered in order to limit the test concurrency. Test set partitioning is used to divide a test set into several test sequences so that they can be tightly packed into the two-dimensional space of power and time. The partitioning of test sets is integrated into the test scheduling process. A heuristic has been developed to find an efficient test schedule which leads to reduced expected test time. Experimental results have shown the efficiency of the proposed test scheduling approach.

  • 91.
    He, Zhiyuan
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Simulation-Driven Thermal-Safe Test Time Minimization for System-on-Chip2008In: Asian Test Symposium, 2008. ATS '08, IEEE Computer Society, 2008, p. 283-288Conference paper (Refereed)
    Abstract [en]

      Thermal safety has become a major challenge to the testing of systems-on-chip with deep sub-micron technologies. In order to avoid overheating the devices under test while reducing test application times, new techniques are needed. In this paper, we propose a test scheduling technique to minimize the test application time such that the temperatures of individual cores are kept below a given limit. The proposed approach takes into account thermal influences between cores, and thus accurate temperature evolution information of all cores in a system-on-chip is needed for the test scheduling. In order to avoid overheating, we have employed a thermal simulation driven scheduling algorithm, in which instantaneous thermal simulation results are used to guide the partitioning of test sets into test sub-sequences and to determine cooling periods inserted between the partitions. Furthermore, the partitioned test sets for different cores are interleaved such that a cooling period reserved for one core can be utilized for the test-data transportations and test applications for other cores. Experimental results have shown that by using the proposed technique, the test application time is minimized and the temperatures of cores under test are kept below the temperature limit during the entire test process.

  • 92.
    He, Zhiyuan
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Thermal-Aware SoC Test Scheduling2010In: Design and Test Technology for Dependable Systems-on-chip / [ed] Raimund Ubar, Jaan Raik, Heinrich Theodor Vierhaus, Information Science Publishing , 2010Chapter in book (Other academic)
    Abstract [en]

    Designing reliable and dependable embedded systems has become increasingly important as the failure of these systems in an automotive, aerospace or nuclear application can have serious consequences.

    Design and Test Technology for Dependable Systems-on-Chip covers aspects of system design and efficient modelling, and also introduces various fault models and fault mechanisms associated with digital circuits integrated into System on Chip (SoC), Multi-Processor System-on Chip (MPSoC) or Network on Chip (NoC). This book provides insight into refined "classical" design and test topics and solutions for IC test technology and fault-tolerant systems.

  • 93.
    He, Zhiyuan
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Thermal-Aware Test Scheduling for Core-based SoC in an Abort-on-First-Fail Test Environment2009In: 12th EUROMICRO Conference on Digital System Design (DSD), Patras, Greece, August 27-29, 2009., IEEE COMPUTER SOC , 2009, p. 239-246Conference paper (Refereed)
    Abstract [en]

    Long test application time and high temperature have become two major issues of system-on-chip (SoC) test. In order to minimize test application times and avoid overheating during tests, we propose a thermal-aware test scheduling technique for core-based SoC in an abort-on-first-fail (AOFF) test environment. The AOFF environment assumes that the test process is terminated as soon as the first fault is detected, which is usually deployed in volume production test. To avoid high temperature, test sets are partitioned into test sub-sequences which are separated by cooling periods. The proposed test scheduling technique utilizes instantaneous thermal simulation results to guide the partitioning of test sets and to determine the lengths of cooling periods. Experimental results have shown that the proposed technique is efficient to minimize the expected test application time while keeping the temperatures of cores under test below the imposed temperature limit.

  • 94.
    He, Zhiyuan
    et al.
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Peng, Zebo
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Eles, Petru Ion
    Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
    Rosinger, Paul
    School of Electronics and Computer Science University of Southampton.
    Al-Hashimi, Bashir M.
    School of Electronics and Computer Science University of Southampton.
    Thermal-Aware SoC Test Scheduling with Test Set Partitioning and Interleaving2006In: International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT'06), Arlington, Virginia, USA, October 4-6, 2006., Arlington: IEEE Computer Society Press , 2006, p. 477-485Conference paper (Refereed)
    Abstract [en]

    High temperature has become a major problem for system-on-chip testing. In order to reduce the test time while keeping the temperature of the chip under test within a safe range, a thermal-aware test scheduling technique is required. This paper presents an approach to minimize the test time and, at the same time, prevent the temperature of cores under test going over the given upper limit. We employ test set partitioning to divide test sets into shorter test sequences, and add cooling spans between test sequences, so that overheating can be avoided. Moreover, test sequences from different test sets are interleaved, in order to utilize the cooling spans and the test bus bandwidth for test data transportation, hence the total test time is reduced. The test scheduling problem is formulated as a combinatorial optimization problem, and we use constraint logic programming to solve it in order to obtain the optimal solution. Experimental results have shown the efficiency of the proposed approach.

  • 95.
    He, Zhiyuan
    et al.
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Ion Eles, Petru
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Multi-temperature testing for core-based system-on-chip2010In: Proceedings -Design, Automation and Test in Europe, DATE, IEEE , 2010, p. 208-213Conference paper (Refereed)
    Abstract [en]

    Recent research has shown that different defects can manifest themselves as failures at different temperature spectra. Therefore, we need multi-temperature testing which applies tests at different temperature levels. In this paper, we discuss the need and problems for testing core-based systems-on-chip at different temperatures. To address the long test time problem for multitemperature test, we propose a test scheduling technique that generates the shortest test schedules while keeping the cores under test within a temperature interval. Experimental results show the efficiency of the proposed technique.

  • 96.
    Horga, Adrian
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Chattopadhyay, Sudipta
    Singapore University of Technology and Design (SUTD), Information Systems Technology and Design (ISTD), Singapore.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Measurement Based Execution Time Analysis of GPGPU Programs via SE+GA2018Conference paper (Refereed)
    Abstract [en]

    Understanding the execution time is critical for embedded, real-time applications. Worst-case execution time (WCET) is an important metric to check the real-time constraints imposed on embedded applications. For complex execution platforms, such as graphics processing units (GPUs), analysis of WCET imposes great challenges due to the complex characteristics of GPU architecture as well as GPU program semantics. In this paper, we propose GDivAn, a measurement-based WCET analysis tool for arbitrary GPU kernels. GDivAn systematically combines the strength of symbolic execution (SE) and genetic algorithm (GA) to maintain both the scalability and the effectiveness of the analysis process. Our evaluation with several open-source GPU kernels reveals the efficiency of GDivAn.

  • 97.
    Horga, Adrian
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Chattopadhyay, Sudipta
    Singapore University of Technology and Design (SUTD), Information Systems Technology and Design (ISTD).
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Genetic Algorithm Based Estimation of Non–Functional Properties for GPGPU Programs2019In: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165Article in journal (Refereed)
    Abstract [en]

    Non-functional properties, like execution time or memory access information, of programs running on graphics processing unit (GPUs) can raise safety and security concerns. For example, understanding the execution time is critical for embedded and real-time applications. To this end, worst-case execution time (WCET) is an important metric to check the real-time constraints imposed on embedded applications. For complex execution platforms, such as GPUs, analysis of WCET imposes great challenges due to the complex characteristics of GPU architecture as well as GPU program semantics. GPUs also have specific memory access behavior. Observing such memory access behavior may reveal sensitive information (e.g. a secret key). This, in turn, may be exploited to launch a side-channel attack on the underlying program.

    In this paper, we propose GDivAn, a measurement-based analysis framework for investigating the non-functional aspects of GPU programs, specifically, their execution time and side-channel leakage capacity. GDivAn is built upon a novel instantiation of genetic algorithm (GA). Moreover, GDivAn improves the effectiveness of GA using symbolic execution, when possible. Our evaluation with several open-source GPU kernels, including GPU kernels from the OpenSSL and MRTC benchmark suite, reveals the effectiveness of GDivAn both in terms of finding WCET and side-channel leakage.

  • 98.
    Horga, Adrian
    et al.
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Chattopadhyay, Sudipta
    Centre for IT-Security, Privacy and Accountability, Saarland University, Germany.
    Eles, Petru
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Systematic detection of memory related performance bottlenecks in GPGPU programs2016In: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165, Vol. 71, p. 73-87Article in journal (Refereed)
    Abstract [en]

    Graphics processing units (GPUs) pose an attractive choice for designing high-performance and energy-efficient software systems. This is because GPUs are capable of executing massively parallel applications. However, the performance of GPUs is limited by the contention in memory subsystems, often resulting in substantial delays and effectively reducing the parallelism. In this paper, we propose GRAB, an automated debugger to aid the development of efficient GPU kernels. GRAB systematically detects, classifies and discovers the root causes of memory-performance bottlenecks in GPUs. We have implemented GRAB and evaluated it with several open-source GPU kernels, including two real-life case studies. We show the usage of GRAB through improvement of GPU kernels on a real NVIDIA Tegra K1 hardware – a widely used GPU for mobile and handheld devices. The guidance obtained from GRAB leads to an overall improvement of up to 64%.

  • 99.
    Hu, X. Sharon
    et al.
    Univ Notre Dame, IN 46556 USA.
    Ernst, Rolf
    Tech Univ Brunswick, ME USA.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
    Heiser, Gernot
    Univ New South Wales Sydney, Australia.
    Keutzer, Kurt
    Univ Calif Berkeley, CA 94720 USA.
    Kim, Daehyun
    Samsung, South Korea.
    Tohdo, Tetsuya
    DENSO CORP, Japan.
    Machine Learning for Embedded Systems: Hype or Lasting Impact? A Panel at ESWEEK 20172018In: IEEE design & test, ISSN 2168-2356, E-ISSN 2168-2364, Vol. 35, no 6, p. 86-93Article in journal (Other academic)
    Abstract [en]

    n/a

  • 100.
    Izosimov, Viacheslav
    et al.
    Embedded Intelligent Solutions (EIS) By Semcon AB, Linköping, Sweden.
    Eles, Petru Ion
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Peng, Zebo
    Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
    Value-Based Scheduling of Distributed Fault-Tolerant Real-Time Systems with Soft and Hard Timing Constraints2010In: 8th IEEE Workshop on Embedded Systems for Real-TimeMultimedia, Scottsdale, AZ, USA, October 28-29, 2010., IEEE , 2010Conference paper (Refereed)
    Abstract [en]

    We present an approach for scheduling of fault tolerant embedded applications composed of soft and hard real time processes running on distributed embedded systems. The hard processes are critical and must always complete on time. A soft process can complete after its deadline and its completion time is associated with a value function that characterizes its contribution to the quality-of-service of the application. We propose a quasi-static scheduling algorithm to generate a tree of fault-tolerant distributed schedules that maximize the application's quality value and guarantee hard deadlines.

123456 51 - 100 of 265
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf