Related papers: Formalisation and Analysis of Component Dependenci…
This paper presents an Isabelle/HOL+Isar set of theories which allows to specify crypto-based components and to verify their composition properties wrt. cryptographic aspects. We introduce a formalisation of the security property of data…
This paper presents a formal approach to modelling and analysis of data and control flow dependencies between services within remotely deployed distributed systems of services. Our work aims at elaborating for a concrete system, which parts…
This set of theories presents an Isabelle/HOL+Isar formalisation of stream processing components introduces in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of…
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or…
This article provides formal definitions characterizing well-formed composition of components in order to guarantee their safe deployment and execution. Our work focuses on the structural aspects of component composition; it puts together…
The contemporary development of hardware components is a prerequisite for increasing the concentration of computing power. System software is developing at a much slower pace. To use available resources efficiently modeling is required.…
We develop a general formalism for representing and understanding structure in complex systems. In our view, structure is the totality of relationships among a system's components, and these relationships can be quantified using information…
Component-based design paradigm is of paramount importance due to prolific growth in the complexity of modern-day systems. Since the components are developed primarily by multi-party vendors and often assembled to realize the overall…
Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been…
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's…
To analyse cryptographic properties of distributed systems in a systematic way, a formal theory is required. In this paper, we present a theory that allows (1) to specify distributed systems formally, (2) to verify their cryptographic wrt.…
This is an account of the characterization of database dependencies with Formal Concept Analysis.
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using…
Web Services provide interoperable mechanisms for describing, locating and invoking services over the Internet; composition further enables to build complex services out of simpler ones for complex B2B applications. While current studies on…
Service composition has become commonplace nowadays, in large part due to the increased complexity of software and supporting networks. Composition can be of many types, for instance sequential, prioritising, non-deterministic. However, a…
In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were discovered by cross-site data mining on huge databases, and…
The paper presents an explicit state-based modeling approach aimed at modeling Systems of Systems behavior. The approach allows to specify and verify incrementally safety and liveness rules without using model checking techniques. The…
In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature…
We present a formalization of the OSGi component framework. Our formalization is intended to be used as a basis for describing behavior of OSGi based systems. Furthermore, we describe specification formalisms for describing properties of…
An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…