We develop formal foundations for notions and mechanisms needed to support service-oriented computing. Our work builds on recent theoretical advancements in the algebraic structures that capture the way services are orchestrated and in the processes
that formalize the discovery and binding of services to given client applications by means of logical representations of required and provided services. We show how the denotational and the operational semantics specific to conventional logic programming can be generalized using the theory of institutions to address both static and dynamic aspects of service-oriented computing. Our results rely upon a strong analogy between the discovery of a service that can be bound to an application and the search for a clause that can be used for computing an answer to a query; they explore the manner in which requests for external services can be described as service queries, and explain how the computation of their answers can be performed through service-oriented derivatives of unification and resolution, which characterize the binding of services and the reconfiguration of applications.
This paper presents an approach towards specifying and verifying adaptive distributed systems. We here take fault-handling as an example of adaptive behavior and propose a modeling language Sandal for describing fault-prone message-passing systems. O
ne of the unique mechanisms of the language is a linguistic support for abstracting typical faults such as unexpected termination of processes and random loss of messages. The Sandal compiler translates a model into a set of NuSMV modules. During the compilation process, faults specified in the model will be woven into the output. One can thus enjoy full-automatic exhaustive fault-injection without writing faulty behaviors explicitly. We demonstrate the advantage of the language by verifying a model of the two-phase commit protocol under faulty environment.
Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they n
ormally utilize Gentzens original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization which we have found out to be crucial for analyzing proofs. We then evaluate recent developments in tree visualization with regard to these criteria and propose the Sunburst Tree layout as a complement to the traditional tree structure. This layout constructs inferences as concentric circle arcs around the root inference, allowing the user to focus on the proofs structural content. Finally, we describe its integration into ProofTool and explain how it interacts with the Gentzen layout.
35 -
Chris Chapman (Royal Military College of Canada
, Electrical andn Computer Engineering Department
, Kingston
2014
This paper identifies an intrusion surveillance framework which provides an analyst with the ability to investigate and monitor cyber-attacks in a covert manner. Where cyber-attacks are perpetrated for the purposes of espionage the ability to underst
and an adversarys techniques and objectives are an important element in network and computer security. With the appropriate toolset, security investigators would be permitted to perform both live and stealthy counter-intelligence operations by observing the behaviour and communications of the intruder. Subsequently a more complete picture of the attackers identity, objectives, capabilities, and infiltration could be formulated than is possible with present technologies. This research focused on developing an extensible framework to permit the covert investigation of malware. Additionally, a Universal Serial Bus (USB) Mass Storage Device (MSD) based covert channel was designed to enable remote command and control of the framework. The work was validated through the design, implementation and testing of a toolset.
Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its Register-Transfer Level (RTL) implementation. Loop pipelining is one of the most critical and complex transformations employed in behavioral synthesis. Certifyin
g the loop pipelining algorithm is challenging because there is a huge semantic gap between the input sequential design and the output pipelined implementation making it infeasible to verify their equivalence with automated sequential equivalence checking techniques. We discuss our ongoing effort using ACL2 to certify loop pipelining transformation. The completion of the proof is work in progress. However, some of the insights developed so far may already be of value to the ACL2 community. In particular, we discuss the key invariant we formalized, which is very different from that used in most pipeline proofs. We discuss the needs for this invariant, its formalization in ACL2, and our envisioned proof using the invariant. We also discuss some trade-offs, challenges, and insights developed in course of the project.
83 -
Sunil Kumar R (Research Scholar
, Department of Computer Applications
, n Cochin University of Science
2014
There are several centrality measures that have been introduced and studied for real world networks. They account for the different vertex characteristics that permit them to be ranked in order of importance in the network. Betweenness centrality is
a measure of the influence of a vertex over the flow of information between every pair of vertices under the assumption that information primarily flows over the shortest path between them. In this paper we present betweenness centrality of some important classes of graphs.
In the (covariant) topos approach to quantum theory by Heunen, Landsman and Spitters, one associates to each unital C*-algebra, A, a topos T(A) of sheaves on a locale and a commutative C*-algebra, a, within that topos. The Gelfand spectrum of a is a
locale S in this topos, which is equivalent to a bundle over the base locale. We further develop this external presentation of the locale S, by noting that the construction of the Gelfand spectrum in a general topos can be described using geometric logic. As a consequence, the spectrum, seen as a bundle, is computed fibrewise. As a by-product of the geometricity of Gelfand spectra, we find an explicit external description of the spectrum whenever the topos is a functor category. As an intermediate result we show that locally perfect maps compose, so that the externalization of a locally compact locale in a topos of sheaves over a locally compact locale is locally compact, too.
We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component
theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards.
We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys
a bisimulation result, and is suitable for practical model checking.
In this paper we extend and prove in detail the Finite Rank Theorem for connection matrices of graph parameters definable in Monadic Second Order Logic with counting (CMSOL) from B. Godlin, T. Kotek and J.A. Makowsky (2008) and J.A. Makowsky (2009).
We demonstrate its vast applicability in simplifying known and new non-definability results of graph properties and finding new non-definability results for graph parameters. We also prove a Feferman-Vaught Theorem for the logic CFOL, First Order Logic with the modular counting quantifiers.
