enter search term and/or author name
Guest editorial: Special issue on models and methodologies for co-design of embedded systems
Sandeep K. Shukla, Jean-Pierre Talpin
This special issue is based on innovative ideas presented and discussed during the first ACM/IEEE Conference on Formal Methods and Models for Co-Design (MEMOCODE) held at Mont Saint Michel in France during the summer of 2003. Selected papers from the...
Verification of safety properties for parameterized regular systems
David Cachera, Katell Morin-Allory
We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We benefit from the intrinsic regularity of the underlying polyhedral model to handle...
PLTL-partitioned model checking for reactive systems under fairness assumptions
S. Chouali, J. Julliand, P.-A. Masson, F. Bellegarde
We are interested in verifying dynamic properties of finite state reactive systems under fairness assumptions by model checking. The systems we want to verify are specified through a top-down refinement process.In order to deal with the state...
Converging CSP specifications and C++ programming via selective formalism
William B. Gardner
CSP (communicating sequential processes) is a useful algebraic notation for creating a hierarchical behavioral specification for concurrent systems, due to its formal interprocess synchronization and communication semantics. CSP specifications are...
Combining supervisor synthesis and model checking
Roberto Ziller, Klaus Schneider
Model checking and supervisor synthesis have been successful in solving different design problems related to discrete systems in the last decades. In this paper, we analyze some advantages and drawbacks of these approaches and combine them for mutual...
A highly configurable cache for low energy embedded systems
Chuanjun Zhang, Frank Vahid, Walid Najjar
Energy consumption is a major concern in many embedded computing systems. Several studies have shown that cache memories account for about 50% of the total energy consumed in these systems. The performance of a given cache architecture is...
Data space-oriented tiling for enhancing locality
I. Kadayif, M. Kandemir
Improving locality of data references is becoming increasingly important due to increasing gap between processor cycle times and off-chip memory access latencies. Improving data locality not only improves effective memory access time but also reduces...
Instantaneous current modeling in a complex VLIW processor core
Radu Muresan, Catherine Gebotys
Measuring and modeling instantaneous current consumption or current dynamics of a processor is important in embedded system designs, wireless communications, low-energy mobile computing, security of communications, and reliability. In this paper, we...
A reprogrammable customization framework for efficient branch resolution in embedded processors
Peter Petrov, Alex Orailoglu
We present a customization framework for embedded processors which employs the utilization of application-specific information, thus specializing the processor's microarchitecture to the application needs. The increased processor utilization leads to...