IEEE Computer Society DATC
IEEE Circuits and System Society
University of Tokyo, Japan
UC San Diego, USA
Paul Le Guernic
Sandeep Kumar Shukla
Virginia Tech, USA
Similar trends and common problems have emerged lately in the hardware and software industries. In the hardware industry, the rising technological complexity of hardware components (e.g., the “system-on-a-chip”) coupled with requirements for increased performance and shortened time to market have produced a growing demand for higher levels of abstraction in the hardware design process. The response has been a trend in hardware design to more abstract modeling, using variants, such as SystemC and SpecC, of general-purpose programming languages, such as C and C++. Similarly, in the software industry, the rising complexity of software systems coupled with the need for increased performance and lower software costs have led important sectors of the software industry, e.g., avionics companies, to adopt model-based approaches to software development and to increase usage of modeling languages such as UML.
Moreover, the growing need for new services in the hardware industry has led to new techniques for the adaptation and integration of existing hardware components. Similarly, in the software industry, the increasing availability of standard software components, such as middleware, has produced an urgent need to compose standard software components so that the composite system is guaranteed to deliver its services reliably and in a manner that satisfies critical properties, such as safety and security.
To adapt designs and to integrate components in a cost-effective and efficient manner, new techniques and methodologies are needed for constructing trustworthy systems from the existing base of standard hardware and software components. The abstract models, formal languages, and formal analysis techniques produced by formal methods research should provide a sound methodological basis for the high level modeling, design, and development of both hardware and software and for adapting and integrating existing components to meet new requirements.
The goal of MEMOCODE 2004, the second in a series of international conferences, is to gather together researchers and software and hardware practitioners to explore ways in which software and hardware design can exploit research results in formal methods. Papers, panel proposals, and tutorial proposals are invited on topics relevant to the application of formal methods to hardware and software design. These topics include formal specification languages, formal models, model checking, theorem proving, specification-based testing, compositional methods, methodologies based on formal methods, and rigorous approaches (e.g., refinement) to transforming a hardware or software specification into a reliable, efficient implementation.