First ACM & IEEE International Conference on

Formal Methods and Models for Codesign (MEMOCODE'2003)

Programming models, formal analysis methods and verification techniques for high-level
system design and (re)engineering: towards convergence of formal methods and industrial trends.

June 24th.-26th., 2003 -- Mont Saint-Michel, France

Home page

Aims and scope

Call for papers

Case studies

Aims and scope of MEMOCODE. High-level design and modeling of hardware and embedded hardware/software systems have gained prominence in the face of rising technological complexity, increasing performance requirements, and shortening time to market demands for complex electronic equipments.

Over the last decades, numerous programming models, languages, tools and frameworks have been proposed to design, simulate and validate heterogeneous systems within an abstract and rigorously defined mathematical model. Although formal programming frameworks are usually not amenable to direct engineering use, they provide well-defined mathematical models that yield a rigorous methodological support for the trusted design, automatic validation, and test generation of systems.

The recent introduction of modeling frameworks based on general-purpose programming language variants (SystemC, SpecC, etc) has been viewed by many as a solution to fill the industrial productivity gap in response to growing industry demand for a higher abstraction levels in the system design process. Meanwhile, the installed base of existing IPs adds further requirements for the adaptation of existing IPs with new services within complex integrated architectures, calling for appropriate methodological approaches.

At this stage, a possibility of widening the existing divergence between formal methods and the industrial practice is perceivable. It seems that any useful methodology cannot avoid the industrial trend of using emerging programming languages. But can we bring a convergence between formal methods and these growing trends?

Whereas abstract frameworks are ways to unambiguously model the essense of hardware software systems, to help understand the design, implement formal correctness proofs and predict performances and other metrics; general-purpose languages facilitate programming, reuse and gain from the popularity of C/C++ like languages. As a result, important gaps need to be filled and bridges need to be built between theoretical models of computations and practical experience in general purpose programming based design (exemplified in SystemC, SpecC, and similar frameworks). Languages shall benefit from the rigorousness of models and models shall be enriched by the experience of programming practice.

This contrasted picture calls for debates and discussions towards bringing theory and practice together, and finding a convergence between the two approaches. This naturally yields a focal point of the conference on formal methods (programming and concurrency models, analysis and verification techniques) for hardware/software co-design, as well as on programming languages based system level design methodologies. A focus on formal methods (programming and concurrency models, analysis and verification techniques) for hardware/software codesign, as well as on programming language based design methodology is necessary. The main stream system designers mostly work with general-purpose languages, and a technology transfer of research in formal methods will be the only way to bring about a change in system design practice leading to provably correct system construction

We hope that this conference will bring together experts in the fields of formal modeling and methodology, high level modeling for embedded systems, programming methodologies for system design, and industry experts, and engage them into useful discussions towards this important convergence.