Interactive verification of architectural design patterns in FACTum

DOI10.1007/s00165-019-00488-xzbMath1425.68273OpenAlexW2966848734MaRDI QIDQ2335950

Habtom Kashay Gidey, Diego Marmsoler

Publication date: 18 November 2019

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-019-00488-x

zbMATH Keywords

algebraic specificationinteractive theorem provingHOLIsabellearchitecture verificationarchitecture design patternsFACTum

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

A type language for distributed reactive components governed by communication protocols, Unnamed Item, Runtime verification for dynamic architectures, Interactive verification of architectural design patterns in FACTum

Uses Software

• Coq
• Isabelle
• Rapide
• Isabelle/HOL
• Isabelle/Isar
• NuSMV
• Isar
• HOL
• Reo
• FDR3
• Xtext
• Coinductive
• Archive Formal Proofs
• FACTum
• Dynamic Architectures
• Architectural_Design_Patterns

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modeling dynamic reconfigurations in Reo using high-level replacement systems
• A graph transformation approach to software architecture reconfiguration
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Categorical semantics of parallel program design
• Isabelle/HOL. A proof assistant for higher-order logic
• Ouroboros: a provably secure proof-of-stake blockchain protocol
• Towards a calculus for dynamic architectures
• On the verification of architectural reconfigurations
• NuSMV: A new symbolic model checker
• Structural reconfiguration of systems under behavioral adaptation
• Hierarchical specification and verification of architectural design patterns
• Interactive verification of architectural design patterns in FACTum
• Modeling component connectors in Reo by constraint automata
• Specification and Development of Interactive Systems
• Truly Modular (Co)datatypes for Isabelle/HOL
• Specifying Properties of Dynamic Architectures Using Configuration Traces
• Counting CTL
• Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting
• Communicating sequential processes
• On Activation, Connection, and Behavior in Dynamic Architectures
• Reo: a channel-based coordination model for component composition
• A Model of Dynamic Systems
• FDR3 — A Modern Refinement Checker for CSP
• Types for Proofs and Programs