liu.seSök publikationer i DiVA
Ändra sökning
Avgränsa sökresultatet
1 - 25 av 25
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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.
    Cortes, Luis-Alejandro
    et al.
    Volvo Truck Corporation, Gothenburg, Sweden.
    Eles, Petru Ion
    Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system. Linköpings universitet, Tekniska högskolan.
    Peng, Zebo
    Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system. Linköpings universitet, Tekniska högskolan.
    A Quasi-Static Approach to Minimizing Energy Consumption in Real-Time Systems under Reward Constraints2006Ingår i: 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 2006, IEEE Computer Society, 2006, s. 279-286Konferensbidrag (Refereegranskat)
    Abstract [en]

    In some real-time applications, it is desirable to trade off precision for timeliness. For such systems, considered typically under the Imprecise Computation model, a function assigns reward to the application depending on the amount of computation allotted to it. Also, many such applications run on battery-powered devices where the energy consumption is of utmost importance. We address in this paper the problem of energy minimization for Imprecise-Computation systems that have reward and time constraints. We propose a Quasi-Static (QS) approach that exploits, with low on-line overhead, the dynamic slack that arises from variations in the actual number of execution cycles: first, at design-time, a set of solutions are computed and stored (off-line phase); second, the selection among the precomputed assignments is left for run-time, based on actual values of time and reward (on-line phase).

  • 2.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    An Approach to Reducing Verification Complexity of Real-Time Embedded Systems2002Ingår i: 14th Euromicro Conference on Real-Time Systems ECRTS 2002, Work-in-Progress Session,2002, 2002, s. 45-48Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present an approach to the formal verification of real-time embedded systems by using model checking. We address the verification of systems modeled in a timed Petri net representation and introduce a technique for reducing verification complexity. We translate the Petri net based model into timed automata and make use of availablemodel checking tools to prove the correctness of the system with respect to design properties expressed in the temporal logics CTL and TCTL. Experimental results demonstrate considerable improvements in verification efficiency when the degree of parallelism of the system is considered.

  • 3.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Combining Static and Dynamic Scheduling for Real-Time Systems2004Ingår i: Workshop on Software Analysis and Development for Pervasive Systems SONDA 2004,2004, Southampton, UK: University of Southampton , 2004, s. 32-Konferensbidrag (Refereegranskat)
    Abstract [en]

    We address in this paper the combination of static and dynamic scheduling into an approach called quasi-static scheduling, in the context of real-time systems composed of hard and soft tasks. For the particular problem discussed in this paper, a single static schedule is too pessimistic while a purely dynamic scheduling approach causes a very high on-line overhead. In the proposed quasi-static solution we compute at design-time a set of schedules, and leave 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. The approach is evaluated through synthetic examples.

  • 4.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Definitions of Equivalence for Transformational Synthesis of Embedded Systems2000Ingår i: 6th International Conference on Engineering of Complex Computer Systems ICECCS 2000,2000, Tokyo, Japan: IEEE Computer Society Press , 2000, s. 134-142Konferensbidrag (Refereegranskat)
    Abstract [en]

    Design of embedded systems is a complex task that requires design cycles founded upon formal notation, so that the synthesis from specification to implementation can be carried out systematically. In this paper we present a computational model for embedded systems based on Petri nets called PRES+. It includes an explicit notion of time and allows a concise formulation of models. Tokens, in our notation, hold information and transitionsÑwhen firedÑperform transformation of data. Based on this model we define several notions of equivalence (reachable, behavioral, time, and total), which provide the framework for transformational synthesis of embedded systems. Different representations of an Ethernet network coprocessor are studied in order to illustrate the applicability of PRES+ and the definitions of equivalence on practical systems.

  • 5.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Formal Coverification of Embedded Systems using Model Checking2000Ingår i: 26th Euromicro Conference Digital Systems Design,2000, Maastricht, The Netherlands: IEEE Computer Society Press , 2000, s. 106-113 vol.1Konferensbidrag (Refereegranskat)
    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.

  • 6.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    From Haskell to PRES+ Basic Translation Procedures2001Rapport (Övrigt vetenskapligt)
    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.

  • 7.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Hierarchical Modeling and Verification of Embedded Systems2001Ingår i: Euromicro Symposium on Digital Systems Design,2001, Warsaw, Poland: IEEE Computer Society Press , 2001, s. 63-Konferensbidrag (Refereegranskat)
    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.

  • 8.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Hierarchies for the Modeling and Verification of Embedded Systems2001Rapport (Övrigt vetenskapligt)
    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.

  • 9.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Modeling and formal verification of embedded systems based on a Petri net representation2003Ingår i: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165, Vol. 49, nr 12-15, s. 571-598Artikel i tidskrift (Refereegranskat)
    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.

  • 10.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Modeling and Verification of Embedded Systems using Petri Net based Methods: Application to an Industrial Case2001Rapport (Övrigt vetenskapligt)
    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.

  • 11.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Quasi-Static Assignment of Voltages and Optional Cycles for Maximizing Rewards in Real-Time Systems with Energy Constraints2005Ingår i: 42nd Design Automation Conference,2005, Anaheim, CA, USA: IEEE Computer Society Press , 2005, s. 889-Konferensbidrag (Refereegranskat)
    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.

  • 12.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks2003Rapport (Övrigt vetenskapligt)
    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.

  • 13.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks2005Ingår i: 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications RTCSA05,2005, Hong Kong: IEEE Computer Society Press , 2005, s. 422-Konferensbidrag (Refereegranskat)
    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.

  • 14.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks2003Rapport (Övrigt vetenskapligt)
    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.

  • 15.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks2004Ingår i: Design, Automation and Test in Europe DATE 2004,2004, Paris, France: IEEE Computer Society Press , 2004, s. 1176-Konferensbidrag (Refereegranskat)
    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.

  • 16.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks2003Rapport (Övrigt vetenskapligt)
    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.

  • 17.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks2004Ingår i: The IEEE International Workshop on Electronic Design, Test and Applications DELTA 2004,2004, 2004, s. 115-120Konferensbidrag (Refereegranskat)
    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.

  • 18.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Verification Methodology for Heterogeneous Hardware/Software Systems2000Rapport (Övrigt vetenskapligt)
    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.

  • 19.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Verification of Embedded Systems using a Petri Net based Representation2000Ingår i: 13th International Symposium on System Synthesis ISSS 2000,2000, Madrid, Spain: IEEE Computer Society Press , 2000, s. 149-155Konferensbidrag (Refereegranskat)
    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.

  • 20.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Verification of Heterogeneous Electronic Systems using Model Checking2000Rapport (Övrigt vetenskapligt)
    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.

  • 21.
    Cortes, Luis-Alejandro
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata2002Ingår i: 8th International Conference on Real-Time Computing Systems and Applications RTCSA 2002,2002, 2002, s. 191-199Konferensbidrag (Refereegranskat)
    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.

  • 22.
    Cortés, Luis Alejandro
    Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system. Linköpings universitet, Tekniska högskolan.
    A Petri Net based Modeling and Verification Technique for Real-Time Embedded Systems2001Licentiatavhandling, monografi (Övrigt vetenskapligt)
    Abstract [en]

    Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness.

    In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems.

    First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined 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 real-time 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 ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.

  • 23.
    Cortés, Luis Alejandro
    Linköpings universitet, Institutionen för datavetenskap, ESLAB. Linköpings universitet, Tekniska högskolan.
    Verification and Scheduling Techniques for Real-Time Embedded Systems2005Doktorsavhandling, monografi (Övrigt vetenskapligt)
    Abstract [en]

    Embedded computer systems have become ubiquitous. They are used in a wide spectrum of applications, ranging from household appliances and mobile devices to vehicle controllers and medical equipment. This dissertation deals with design and verification of embedded systems, with a special emphasis on the real-time facet of such systems, where the time at which the results of the computations are produced is as important as the logical values of these results. Within the class of real-time systems two categories, namely hard real-time systems and soft real-time systems, are distinguished and studied in this thesis.

    First, we propose modeling and verification techniques targeted towards hard real-time systems, where correctness, both logical and temporal, is of prime importance. A model of computation based on Petri nets is defined. The model can capture explicit timing information, allows tokens to carry data, and supports the concept of hierarchy. Also, an approach to the formal verification of systems represented in our modeling formalism is introduced, in which model checking is used to prove whether the system model satisfies its required properties expressed as temporal logic formulas. Several strategies for improving verification efficiency are presented and evaluated.

    Second, we present scheduling approaches for mixed hard/soft real-time systems. We study systems that have both hard and soft real-time tasks and for which the quality of results (in the form of utilities) depends on the completion time of soft tasks. Also, we study systems for which the quality of results (in the form of rewards) depends on the amount of computation allotted to tasks. We introduce quasi-static techniques, which are able to exploit at low cost the dynamic slack caused by variations in actual execution times, for maximizing utilities/rewards and for minimizing energy.

    Numerous experiments, based on synthetic benchmarks and realistic case studies, have been conducted in order to evaluate the proposed approaches. The experimental results show the merits and worthiness of the techniques introduced in this thesis and demonstrate that they are applicable on real-life examples.

  • 24.
    Varea, Mauricio
    et al.
    Dept. Electronics and Computer Science University of Southampton.
    Al Hashimi, Bashir M.
    Dept. of Electronics and Computer Science University of Southampton.
    Cortes, Luis-Alejandro
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Symbolic Model Checking of Dual Transition Petri Nets2002Ingår i: 10th International Symposium on HardwareSoftware Codesign CODES 2002,2002, Estes Park, Colorado, USA: IEEE Computer Society Press , 2002, s. 43-Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper describes the formal verification of the recently introduced Dual Transition Petri Net (DTPN) models, using model checking techniques. The methodology presented addresses the symbolic model checking of embedded systems behavioural properties, expressed in either computation tree logics (CTL) or linear temporal logics (LTL). The embedded system specification is given in terms of DTPN models, where elements of the model are captured in a four-module library which implements the behaviour of the model. Key issues in the development of the methodology are the heterogeneity and the nondeterministic nature of the model. This is handled by introducing some modifications in both structure and behaviour of the model, thus reducing the points of nondeterminism. Several features of the methodology are discussed and two examples are given in order to show the validity of the model.

  • 25.
    Varea, Mauricio
    et al.
    Dept. of Electronics and Computer Science University of Southampton.
    Al-Hashimi, Bashir
    Dept. of Electronics and Computer Science University of Southampton.
    Cortes, Luis-Alejandro
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Eles, Petru Ion
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Peng, Zebo
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, ESLAB - Laboratoriet för inbyggda system.
    Dual Flow Nets: Modelling the Control/Data-Flow Relation in Embedded Systems2006Ingår i: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 5, nr 1, s. 54-81Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    This paper addresses the interrelation between control and data flow in embedded system models through a new design representation, called Dual Flow Net (DFN). A modeling formalism with a very close-fitting control and data flow is achieved by this representation, as a consequence of enhancing its underlying Petri net structure. The work presented in this paper does not only tackle the modeling side in embedded systems design, but also the validation of embedded system models through formal methods. Various introductory examples illustrate the applicability of the DFN principles, whereas the capability of the model to with complex designs is demonstrated through the design and verification of a real-life Ethernet coprocessor.

1 - 25 av 25
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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