Refinable Record Structures in Formal Methods
| Autor: | Colin Snook, Michael Butler, Dana Dghaym, Asieh Salehi Fathabadi, Thai Son Hoang |
|---|---|
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | Advances in Model and Data Engineering in the Digitalization Era ISBN: 9783030876562 MEDI Workshops |
| DOI: | 10.1007/978-3-030-87657-9_1 |
| Popis: | State-based formal specifications benefit from data structuring mechanisms, which collate associated properties and efficiently declare complex types. For example, ‘record’ data structures, similar to those used in programming languages, can be built into the concrete syntax of a language as an enhancement over flat data relationships. While this is relatively simple to achieve for a single-level specification, it becomes significantly more involved when the specification language allows for progressive refinement of the data supporting the specification. Individual fields may be added to create sub-records within a refinement and replaced to create refined records during a refinement step. The impact on the ability to verify invariant and refinement proof obligations must be considered. Here we describe a record structuring syntax that includes notions of extension and inheritance that can be used in a refinement-based formal method. We illustrate the approach using extensions to the Event-B formal method. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|