| Scope Proposal for a tutorial at ETAPS’99 Verification of Parametric Systems or Monadic 2 nd Order Logic in Practice (2008) | |||||||||||||||
Abstract | |||||||||||||||
| In this tutorial we intend to present M2L(Str) as an adequate logic for modelling different classes of parametric systems, discuss how a verification environment for this kind of systems can be designed and realized, and show the fielded use of both the logic and its tools for the specification, verification, and synthesis of relevant classes of parametric systems. The detailed discussion of specific application profiles, some of which apparently out of the scope of the proposed methodology, will illustrate the remarkable modeling power of M2L(Str). This power, which marks it as a good candidate formalism for hardware/software codesign, combined with its fully automatic verification feature, indicate its high potential to enter industrial practice. Detailed Organization of the Tutorial The planned organization follows closely the outline of the content (see p. 3), and will be structured as follows: 1. Motivation (with | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||