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 |
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.
|