SwePub - sökning: WFRF:(Peng Zebo 1958 )

Numrering	Referens	Omslagsbild	Hitta
1.	Aminifar, Amir, et al. (författare) Control-Quality Driven Design of Embedded Control Systems with Stability Guarantees 2018 Ingår i: IEEE Design and Test. - : IEEE. - 2168-2356 .- 2168-2364. ; 35:4, s. 38-46 Tidskriftsartikel (refereegranskat)abstract Today, the majority of control applications in embedded systems, e.g., in the automotive domain, are implemented as software tasks on shared platforms. Ignoring implementation impacts during the design of embedded control systems results in complex timing behaviors that may lead to poor performance and, in the worst case, instability of control applications. This article presents a methodology for implementation-aware design of high-quality and stable embedded control systems on shared platforms with complex timing behaviors.
2.	Andrei, Alexandru, 1977-, et al. (författare) Overhead-Conscious Voltage Selection for Dynamic and Leakage Energy Reduction of Time-Constrained Systems 2004 Ingår i: Design, Automation and Test in Europe DATE 2004,2004. - Paris, France : IEEE Computer Society Press. - 0769520855 ; , s. 518- Konferensbidrag (refereegranskat)abstract Dynamic voltage scaling and adaptive body biasing have been shown to reduce dynamic and leakage power consumption effectively. In this paper, we optimally solve the combined supply voltage and body bias selection problem for multi-processor systems with imposed time constraints, explicitly taking into account the transition overheads implied by changing voltage levels. Both energy and time overheads are considered. We investigate the continuous voltage scaling as well as its discrete counterpart, and we prove NP-hardness in the discrete case. Furthermore, the continuous voltage scaling problem is formulated and solved using nonlinear programming with polynomial time complexity, while for the discrete problem we use mixed integer linear programming. Extensive experiments, conducted on several benchmarks and a real-life example, are used to validate the approaches.
3.	Andrei, Alexandru, 1977-, et al. (författare) Overhead-Conscious Voltage Selection for Dynamic and Leakage Energy Reduction of Time-Constrained Systems 2005 Ingår i: IEE Proceedings - Computers and digital Techniques. - : IEEE. - 1350-2387 .- 1359-7027. ; 152:01, s. 28-38 Tidskriftsartikel (refereegranskat)abstract Dynamic voltage scaling and adaptive body biasing have been shown to reduce dynamic and leakage power consumption effectively. In this paper, we optimally solve the combined supply voltage and body bias selection problem for multi-processor systems with imposed time constraints, explicitly taking into account the transition overheads implied by changing voltage levels. Both energy and time overheads are considered. We investigate the continuous voltage scaling as well as its discrete counterpart, and we prove NP-hardness in the discrete case. Furthermore, the continuous voltage scaling problemis formulated and solved using nonlinear programming with polynomial time complexity, while for the discrete problem we use mixed integer linear programming. Extensive experiments, conducted on several benchmarks and a real-life example, are used to validate the approaches.
4.	Andrei, Alexandru, 1977-, et al. (författare) Predictable Implementation of Real-Time Applications on Multiprocessor Systems on Chip 2008 Ingår i: VLSI Design, 2008. VLSID 2008. - : IEEE Computer Society. - 0769530834 - 9780769530833 ; , s. 103-110 Konferensbidrag (refereegranskat)abstract Worst-case execution time (WCET) analysis and, in general, the predictability of real-time applications implemented on multiprocessor systems has been addressed only in very restrictive and particular contexts. One important aspect that makes the analysis difficult is the estimation of the system-s communication behavior. The traffic on the bus does not solely originate from data transfers due to data dependencies between tasks, but is also affected by memory transfers as result of cache misses. As opposed to the analysis performed for a single processor system, where the cache miss penalty is constant, in a multiprocessor system each cache miss has a variable penalty, depending on the bus contention. This affects the tasks- WCET which, however, is needed in order to perform system scheduling. At the same time, the WCET depends on the system schedule due to the bus interference. In this context, we propose, for the first time, an approach to worst-case execution time analysis and system scheduling for real-time applications implemented on multiprocessor SoC architectures.
5.	Andrei, Alexandru, 1977-, et al. (författare) Quasi-Static Voltage Scaling for Energy Minimization with Time Constraints 2005 Ingår i: Design Automation and Test in Europe Conference DATE 2005,2005. - Munich, Germany : IEEE Computer Society Press. - 0769522882 ; , s. 514- Konferensbidrag (refereegranskat)
6.	Andrei, Alexandru, 1977-, et al. (författare) Simultaneous Communication and Processor Voltage Scaling for Dynamic and Leakage Energy Reduction in Time-Constrained Systems 2004 Ingår i: International Conference on Computer Aided Design ICCAD 2004,2004. - San Jose, USA : IEEE Computer Society Press. - 0780387023 ; , s. 362- Konferensbidrag (refereegranskat)abstract In this paper, we propose a new technique for the combined voltage scaling of processors and communication links, taking into account dynamic as well as leakage power consumption. The voltage scaling technique achieves energy efficiency by simultaneously scaling the supply and body bias voltages in the case of processors and buses with repeaters, while energy efficiency on fat wires is achieved through dynamic voltage swing scaling. We also introduce a set of accurate communication models for the energy estimation of voltage scalable embedded systems. In particular, we demonstrate that voltage scaling of bus repeaters and dynamic adaption of the voltage swing on fat wires can significantly influence the system's energy consumption. Experimental results, conducted on numerous generated benchmarks and a real-life example, demonstrate that substantial energy savings can be achieved with the proposed techniques.
7.	Andrei, Alexandru, 1977-, et al. (författare) Voltage Selection for Time-Constrained Multiprocessor Systems on Chip 2007 Ingår i: Designing Embedded Processors: A Low Power Perspective. - Dordrecht : Springer. - 9781402058684 - 1402058683 ; , s. 259-286 Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract As we embrace the world of personal, portable, and perplexingly complex digital systems, it has befallen upon the bewildered designer to take advantage of the available transistors to produce a system which is small, fast, cheap and correct, yet possesses increased functionality. Increasingly, these systems have to consume little energy.Designers are increasingly turning towards small processors, which are low power, and customize these processors both in software and hardware to achieve their objectives of a low power system, which is verified, and has short design turnaround times. Designing Embedded Processors examines the many ways in which processor based systems are designed to allow low power devices.It looks at processor design methods, memory optimization, dynamic voltage scaling methods, compiler methods, and multi processor methods. Each section has an introductory chapter to give a breadth view, and have a few specialist chapters in the area to give a deeper perspective. The book provides a good starting point to engineers in the area, and to research students embarking upon the exciting area of embedded systems and architectures.
8.	Bao, Min, 2000-, et al. (författare) Temperature-Aware Task Mapping for Energy Optimization with Dynamic Voltage Scaling 2008 Ingår i: 11th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems, 2008. - : IEEE Computer Society. - 9781424422760 ; , s. 44-49 Konferensbidrag (refereegranskat)abstract Temperature has become an important issue in nowadays MPSoCs design due to the ever increasing power densities and huge energy consumption. This paper proposes a temperature-aware task mapping technique for energy optimization in systems with dynamic voltage selection capability. It evaluates the efficiency of this technique, based on the analysis of the factors that can influence the potential gains that can be expected from such a technique, compared to a task mapping approach that ignores temperature.
9.	Bao, Min, 2000-, et al. (författare) Temperature-Aware Voltage Selection for Energy Optimization 2008 Ingår i: Design, Automation and Test in Europe, 2008. - : IEEE. - 9783981080131 ; , s. 1083-1086 Konferensbidrag (refereegranskat)abstract This paper proposes a temperature-aware dynamic voltage selection technique for energy minimization and presents a thorough analysis of the parameters that influence the potential gains that can be expected from such a technique, compared to a voltage selection approach that ignores temperature.
10.	Bengtsson, Tomas, et al. (författare) Off-line Testing of Delay Faults in NoC Interconnects 2006 Ingår i: 9th EUROMICRO Conference on Digital System Design. - : IEEE Computer Society. - 0769526098 ; , s. 677-680 Konferensbidrag (refereegranskat)abstract Testing of high density SoCs operating at high clock speeds in an important but difficult problem. Many faults, like delay faults, in such sub-micron chips may only appear when the chip works at normal operating speed. In this paper, we propose a methodology for at-speed testing of delay faults in links connecting two distinct clock domains in a SoC. We give an analytical analysis about the efficiency of this method. We also propose a simple digital hardware structure for the receiver end of the link under test to detect delay faults. It is possible to extend our method to combine it with functional testing of the link and adapt it for on-line testing.
11.	Cortes, Luis-Alejandro, 1972-, et al. (författare) A Quasi-Static Approach to Minimizing Energy Consumption in Real-Time Systems under Reward Constraints 2006 Ingår i: 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 2006. - : IEEE Computer Society. - 0769526764 ; , s. 279-286 Konferensbidrag (refereegranskat)abstract 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).
12.	Cortes, Luis-Alejandro, 1972-, et al. (författare) An Approach to Reducing Verification Complexity of Real-Time Embedded Systems 2002 Ingår i: 14th Euromicro Conference on Real-Time Systems ECRTS 2002, Work-in-Progress Session,2002. ; , s. 45-48 Konferensbidrag (refereegranskat)abstract 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.
13.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Combining Static and Dynamic Scheduling for Real-Time Systems 2004 Ingår i: Workshop on Software Analysis and Development for Pervasive Systems SONDA 2004,2004. - Southampton, UK : University of Southampton. ; , s. 32- Konferensbidrag (refereegranskat)abstract 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.
14.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Definitions of Equivalence for Transformational Synthesis of Embedded Systems 2000 Ingår i: 6th International Conference on Engineering of Complex Computer Systems ICECCS 2000,2000. - Tokyo, Japan : IEEE Computer Society Press. - 076950583X ; , s. 134-142 Konferensbidrag (refereegranskat)abstract 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.
15.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Formal Coverification of Embedded Systems using Model Checking 2000 Ingår i: 26th Euromicro Conference Digital Systems Design,2000. - Maastricht, The Netherlands : IEEE Computer Society Press. - 0769507808 ; , s. 106-113 vol.1 Konferensbidrag (refereegranskat)abstract 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.
16.	Cortes, Luis-Alejandro, 1972-, et al. (författare) From Haskell to PRES+ Basic Translation Procedures 2001 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
17.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Hierarchical Modeling and Verification of Embedded Systems 2001 Ingår i: Euromicro Symposium on Digital Systems Design,2001. - Warsaw, Poland : IEEE Computer Society Press. ; , s. 63- Konferensbidrag (refereegranskat)abstract 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.
18.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Hierarchies for the Modeling and Verification of Embedded Systems 2001 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
19.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Modeling and Verification of Embedded Systems using Petri Net based Methods : Application to an Industrial Case 2001 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
20.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Quasi-Static Assignment of Voltages and Optional Cycles for Maximizing Rewards in Real-Time Systems with Energy Constraints 2005 Ingår i: 42nd Design Automation Conference,2005. - Anaheim, CA, USA : IEEE Computer Society Press. - 1595930582 ; , s. 889- Konferensbidrag (refereegranskat)abstract 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.
21.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks 2003 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
22.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Quasi-Static Scheduling for Multiprocessor Real-Time Systems with Hard and Soft Tasks 2005 Ingår i: 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications RTCSA05,2005. - Hong Kong : IEEE Computer Society Press. - 0769523463 ; , s. 422- Konferensbidrag (refereegranskat)abstract 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.
23.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks 2003 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
24.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Quasi-Static Scheduling for Real-Time Systems with Hard and Soft Tasks 2004 Ingår i: Design, Automation and Test in Europe DATE 2004,2004. - Paris, France : IEEE Computer Society Press. - 0769520855 ; , s. 1176- Konferensbidrag (refereegranskat)abstract 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.
25.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks 2003 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
26.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Static Scheduling of Monoprocessor Real-Time Systems composed of Hard and Soft Tasks 2004 Ingår i: The IEEE International Workshop on Electronic Design, Test and Applications DELTA 2004,2004. - 0769520812 ; , s. 115-120 Konferensbidrag (refereegranskat)abstract 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.
27.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Verification Methodology for Heterogeneous Hardware/Software Systems 2000 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
28.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Verification of Embedded Systems using a Petri Net based Representation 2000 Ingår i: 13th International Symposium on System Synthesis ISSS 2000,2000. - Madrid, Spain : IEEE Computer Society Press. - 0769507654 ; , s. 149-155 Konferensbidrag (refereegranskat)abstract 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.
29.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Verification of Heterogeneous Electronic Systems using Model Checking 2000 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
30.	Cortes, Luis-Alejandro, 1972-, et al. (författare) Verification of Real-Time Embedded Systems using Petri Net Models and Timed Automata 2002 Ingår i: 8th International Conference on Real-Time Computing Systems and Applications RTCSA 2002,2002. ; , s. 191-199 Konferensbidrag (refereegranskat)abstract 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.
31.	Eles, Petru Ion, 1954-, et al. (författare) Report on Early DfT Support 2002 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
32.	Eles, Petru Ion, 1954-, et al. (författare) Scheduling of Conditional Process Graphs for the Synthesis of Embedded Systems 2008. - 1 Ingår i: Design, Automation, and Test in Europe: The Most Influential Papers of 10 Years DATE. - Dordrecht, The Netherlands : Springer. - 9781402064876 ; , s. 15-29 Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract 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.
33.	Eles, Petru Ion, 1954-, et al. (författare) Synthesis of Fault-Tolerant Embedded Systems 2008 Ingår i: Design, Automation and Test in Europe, 2008.. - Munich, Germany : IEEE. - 9783981080131 ; , s. 960-965, s. 1117-1122 Konferensbidrag (refereegranskat)abstract 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.
34.	Ganjei, Zeinab, 1989- (författare) Parameterized Verification of Synchronized Concurrent Programs 2021 Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract There is currently an increasing demand for concurrent programs. Checking the correctness of concurrent programs is a complex task due to the interleavings of processes. Sometimes, violation of the correctness properties in such systems causes human or resource losses; therefore, it is crucial to check the correctness of such systems. Two main approaches to software analysis are testing and formal verification. Testing can help discover many bugs at a low cost. However, it cannot prove the correctness of a program. Formal verification, on the other hand, is the approach for proving program correctness. Model checking is a formal verification technique that is suitable for concurrent programs. It aims to automatically establish the correctness (expressed in terms of temporal properties) of a program through an exhaustive search of the behavior of the system. Model checking was initially introduced for the purpose of verifying finite‐state concurrent programs, and extending it to infinite‐state systems is an active research area.In this thesis, we focus on the formal verification of parameterized systems. That is, systems in which the number of executing processes is not bounded a priori. We provide fully-automatic and parameterized model checking techniques for establishing the correctness of safety properties for certain classes of concurrent programs. We provide an open‐source prototype for every technique and present our experimental results on several benchmarks.First, we address the problem of automatically checking safety properties for bounded as well as parameterized phaser programs. Phaser programs are concurrent programs that make use of the complex synchronization construct of Habanero Java phasers. For the bounded case, we establish the decidability of checking the violation of program assertions and the undecidability of checking deadlock‐freedom. For the parameterized case, we study different formulations of the verification problem and propose an exact procedure that is guaranteed to terminate for some reachability problems even in the presence of unbounded phases and arbitrarily many spawned processes. Second, we propose an approach for automatic verification of parameterized concurrent programs in which shared variables are manipulated by atomic transitions to count and synchronize the spawned processes. For this purpose, we introduce counting predicates that related counters that refer to the number of processes satisfying some given properties to the variables that are directly manipulated by the concurrent processes. We then combine existing works on the counter, predicate, and constrained monotonic abstraction and build a nested counterexample‐based refinement scheme to establish correctness. Third, we introduce Lazy Constrained Monotonic Abstraction for more efficient exploration of well‐structured abstractions of infinite‐state non‐monotonic systems. We propose several heuristics and assess the efficiency of the proposed technique by extensive experiments using our open‐source prototype. Lastly, we propose a sound but (in general) incomplete procedure for automatic verification of safety properties for a class of fault‐tolerant distributed protocols described in the Heard‐Of (HO for short) model. The HO model is a popular model for describing distributed protocols. We propose a verification procedure that is guaranteed to terminate even for unbounded number of the processes that execute the distributed protocol.
35.	Ganjei, Zeinab, 1989-, et al. (författare) Verifying Safety of Parameterized Heard-Of Algorithms 2021 Konferensbidrag (refereegranskat)abstract We consider the problem of automatically checking safety properties of fault-tolerant distributed algorithms. We express the considered class of distributed algorithms in terms of the Heard-Of Model where arbitrary many processes proceed in infinite rounds in the presence of failures such as message losses or message corruptions. We propose, for the considered class, a sound but (in general) incomplete procedure that is guaranteed to terminate even in the presence of unbounded numbers of processes. In addition, we report on preliminary experiments for which either correctness is proved by our approach or a concrete trace violating the considered safety property is automatically found.
36.	Goloubeva, Olga, et al. (författare) Final Report on Project Results 2002 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
37.	Goloubeva, Olga, et al. (författare) Report on Dissemination Plan 2002 Rapport (övrigt vetenskapligt/konstnärligt)abstract 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.
38.	He, Zhiyuan, 1976-, et al. (författare) A heuristic for thermal-safe SoC test scheduling 2007 Ingår i: IEEE International Test Conference, 2007. - : IEEE. - 9781424411276 ; , s. 116-125 Konferensbidrag (refereegranskat)abstract 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.
39.	He, Zhiyuan, 1976-, et al. (författare) Hybrid BIST Test Scheduling Based on Defect Probabilities 2004 Ingår i: 2004 IEEE Asian Test Symposium ATS 2004,2004. - Kenting, Taiwan : IEEE Computer Society Press. - 0769522351 ; , s. 230- Konferensbidrag (refereegranskat)abstract 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.
40.	He, Zhiyuan, 1976-, et al. (författare) Power Constrained and Defect-Probability Driven SoC Test Scheduling with Test Set Partitioning 2006 Ingår i: Design Automation and Test in Europe Conference DATE 2006,2006. - Munich, Germany : IEEE Computer Society Press. ; , s. 291- Konferensbidrag (refereegranskat)abstract 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.
41.	He, Zhiyuan, 1976-, et al. (författare) Power-Constrained Hybrid BIST Test Scheduling in an Abort-on-First-Fail Test Environment 2005 Ingår i: 8th Euromicro Conference on Digital System Design DSD2005,2005. - Porto, Portugal : IEEE Computer Society Press. - 0769524338 ; , s. 83- Konferensbidrag (refereegranskat)abstract 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.
42.	He, Zhiyuan, 1976-, et al. (författare) Simulation-Driven Thermal-Safe Test Time Minimization for System-on-Chip 2008 Ingår i: Asian Test Symposium, 2008. ATS '08. - : IEEE Computer Society. - 9780769533964 ; , s. 283-288 Konferensbidrag (refereegranskat)abstract 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.
43.	He, Zhiyuan, 1976-, et al. (författare) Thermal-Aware SoC Test Scheduling with Test Set Partitioning and Interleaving 2006 Ingår i: <em>International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT'06), Arlington, Virginia, USA, October 4-6, 2006.</em>. - Arlington : IEEE Computer Society Press. - 076952706X ; , s. 477-485 Konferensbidrag (refereegranskat)abstract 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.
44.	Horga, Adrian, 1989-, et al. (författare) Measurement Based Execution Time Analysis of GPGPU Programs via SE+GA 2018 Konferensbidrag (refereegranskat)abstract 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.
45.	Horga, Adrian, 1989- (författare) Performance and Security Analysis for GPU-Based Applications 2022 Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract Graphics Processing Units (GPUs) are becoming more and more prevalent in general-purpose computing. GPUs are used in areas from embedded systems to super-computing. With applications ranging from fluid dynamics simulations to image processing, machine learning, and encryption, GPU programs need to satisfy not only performance requirements but also various other non-functional constraints. Besides the aspects regarding performance, also security and the worst case execution time (WCET) need to be considered for such GPU applications. In our work, we study such non-functional properties and present approaches to detect and solve issues regarding them.First, we focus on the performance of GPU applications by detecting cache related performance bottlenecks. We detect the root causes of such bottlenecks and provide solutions to reduce their negative impact on performance. We also discuss and compare the impact of cache replacement policies and thread scheduling policies on the performance of GPU applications.Then, we present a measurement-based technique, which combines symbolic execution and genetic algorithms, and is used for estimating the WCET of GPU programs. Our proposed technique helps to produce test inputs that lead towards the WCET of a program. We also propose solutions to alleviate the inherent complexity of GPU programs due to branching behavior and high number of threads running in parallel.In continuation, we propose a technique to expose the side-channel leakage of shared memory in GPU implementations of cryptographic algorithms. We evaluate the robustness of such algorithms in the context of shared memory side-channel leakage. Also, we discuss the security and side-channel leakage for different implementations of the same algorithm.Finally, a formal approach is presented for the detection of GPU shared memory bank conflicts. We explore and discuss the impact of such conflicts on the performance and security of GPU applications. We show how our approach can help in producing inputs that can lead towards the WCET. We also discuss how our approach can be used to evaluate the leakage of the shared memory side-channel for GPU implementations of cryptographic algorithms.
46.	Horga, Adrian, 1989-, et al. (författare) Symbolic identification of shared memory based bank conflicts for GPUs 2022 Ingår i: Journal of systems architecture. - Amsterdam, Netherlands : Elsevier. - 1383-7621 .- 1873-6165. ; 127 Tidskriftsartikel (refereegranskat)abstract Graphic processing units (GPUs) are routinely used for general purpose computations to improve performance. To achieve the sought performance gains, care must be invested in fine tuning the way GPU programs interact with the underlying architecture, accounting for the shared memory bank conflicts and the entailed shared memory transactions. Uncovering inputs leading to particular bank conflicts can turn out to be quite hard given the intricacy of the access patterns and their dependence on the inputs. We propose a symbolic execution based framework to systematically uncover shared memory bank conflicts, to propose inputs to realize a given number of shared memory transactions, and to refute the existence of such inputs if the number of shared memory transactions is impossible to achieve during the execution. This allows programmers to more formally reason about the shared memory conflicts and to validate their impact on performance and security. We have implemented our approach and report on our experiments to explore its usefulness towards performance enhancement and quantifying shared memory side-channel leakage in security applications.
47.	Izosimov, Viacheslav, 1980-, et al. (författare) Design Optimization of Time- and Cost-Constrained Fault-Tolerant Distributed Embedded Systems 2005 Ingår i: Design Automation and Test in Europe Conference DATE 2005,2005. - Munich, Germany : IEEE Computer Society Press. - 0769522882 ; , s. 864- Konferensbidrag (refereegranskat)abstract In this paper we present an approach to the design optimization of fault-tolerant embedded systems for safety-critical applications. Processes are statically scheduled and communications are performed using the time-triggered protocol. We use process re-execution and replication for tolerating transient faults. Our design optimization approach decides the mapping of processes to processors and the assignment of fault-tolerant policies to processes such that transient faults are tolerated and the timing constraints of the application are satisfied. We present several heuristics which are able to find fault-tolerant implementations given a limited amount of resources. The developed algorithms are evaluated using extensive experiments, including a real-life example.
48.	Izosimov, Viacheslav, 1980-, et al. (författare) Mapping of Fault-Tolerant Applications with Transparency on Distributed Embedded Systems 2006 Ingår i: 9th Euromicro Conference on Digital System Design,2006. - Dubrovnik : IEEE Computer Society Press. - 0769526098 ; , s. 313- Konferensbidrag (refereegranskat)abstract In this paper we present an approach for the mapping optimization of fault-tolerant embedded systems for safety-critical applications. Processes and messages are statically scheduled. Process re-execution is used for recovering from multiple transient faults. We call process recovery transparent if it does not affect operation of other processes. Transparent recovery has the advantage of fault containment, improved debugability and less memory needed to store the fault-tolerant schedules. However, it will introduce additional delays that can lead to violations of the timing constraints of the application. We propose an algorithm for the mapping of fault-tolerant applications with transparency. The algorithm decides a mapping of processes on computation nodes such that the application is schedulable and the transparency properties imposed by the designer are satisfied. The mapping algorithm is driven by a heuristic that is able to estimate the worst-case schedule length and indicate whether a certain mapping alternative is schedulable.
49.	Izosimov, Viacheslav, 1980-, et al. (författare) Scheduling of Fault-Tolerant Embedded Systems with Soft and Hard Timing Constraints 2008 Ingår i: Design, Automation, and Test in Europe DATE 2008,2008. - Munich, Germany : IEEE Computer Society Press. - 9783981080131 - 9783981080148 ; , s. 915- Konferensbidrag (refereegranskat)abstract In this paper we present an approach to the synthesis of fault-tolerant schedules for embedded applications with soft and hard real-time constraints. We are interested to guarantee the deadlines for the hard processes even in the case of faults, while maximizing the overall utility. We use time/utility functions to capture the utility of soft processes. A single static schedule computed off-line is not fault tolerant and is pessimistic in terms of utility, while a purely online approach, which computes a new schedule every time a process fails or completes, incurs an unacceptable overhead. Thus, we use a quasi-static scheduling strategy, where a set of schedules is synthesized off-line and, at run time, the scheduler will select the right schedule based on the occurrence of faults and the actual execution times of processes. The proposed schedule synthesis heuristics have been evaluated using extensive experiments.
50.	Izosimov, Viacheslav, 1980-, et al. (författare) Synthesis of Fault-Tolerant Embedded Systems with Checkpointing and Replication 2006 Ingår i: 3rd IEEE Intl. Workshop on Electronic Design, Test Applications DELTA,2006. - Kuala Lumpur, Malaysia : IEEE Computer Society Press. - 0769525008 ; , s. 440- Konferensbidrag (refereegranskat)abstract We present an approach to the synthesis of fault-tolerant hard real-time systems for safety-critical applications. We use checkpointing with rollback recovery and active replication for tolerating transient faults. Processes are statically scheduled and communications are performed using the time-triggered protocol. Our synthesis approach decides the assignment of fault-tolerance policies to processes, the optimal placement of checkpoints and the mapping of processes to processors such that transient faults are tolerated and the timing constraints of the application are satisfied. We present several synthesis algorithms which are able to find fault-tolerant implementations given a limited amount of resources. The developed algorithms are evaluated using extensive experiments, including a real-life example.

Skapa referenser, mejla, bekava och länka

Länka till träfflistan

Träfflista för sökning "WFRF:(Peng Zebo 1958 ) "

Avgränsa träffmängd

År