Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunctions and infinite disjunctions. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr’s theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.

The powerset monad on the category of sets does not distribute over itself. Nevertheless a weaker form of distributive law of the powerset monad over itself exists and it essentially stems from the canonical Egli-Milner extension of the powerset to the category of relations. On the other hand, any regular category yields a category of relations, and some regular categories also possess a powerset-like monad, as is the Vietoris monad on compact Hausdorff spaces. We derive the Egli-Milner extension in three different frameworks : sets, toposes, and compact Hausdorff spaces. We prove that it corresponds to a monotone weak distributive law in each case by showing that the multiplication extends to relations but the unit does not. We provide an application to coalgebraic determinization of alternating automata.

Summary In the context of testing from algebraic specifications, test cases are ground formulas chosen amongst the ground semantic consequences of the specification, according to some possible additional observability conditions. A test set is said to be exhaustive if every programmePpassing all the tests is correct and if for every incorrect programmeP, there exists a test case on whichPfails. Because correctness can be proved by testing on such a test set, it is an appropriate basis for the selection of a test set of practical size. The largest candidate test set is the set of observable consequences of the specification. However, depending on the nature of specifications and programmes, this set is not necessarily exhaustive. In this paper, we study conditions to ensure the exhaustiveness property of this set for several algebraic formalisms (equational, conditional positive, quantifier free and with quantifiers) and several test hypotheses. Copyright © 2016 John Wiley & Sons, Ltd.

Modern industrial systems are often large and distributed. Consequently, building the test harness for them can be technically challenging. A compositional approach attempts to overcome this problem by partitioning the system into smaller parts easier to test separately. And in particular, compositionality helps to avoid as much as possible testing the whole monolithic system thanks to mathematical results which relate the global correctness of the system to the correctness of its constituent parts. In this paper, we present a compositionality result for model-based testing in the setting of the conformance relation tioco which is dedicated to timed systems. We show how to exploit this result in practice by extending a previously defined symbolic testing framework.

We coalgebraically define a unified semantics for systems with an emphasis on the notion of time. Such a semantics intends to formalize system that underly system engineering (i.e. the discipline focusing on the integration mastery of large industrial systems).Moreover, we give a formal meaning to another important aspect of systems engineering: system requirements, constraining the expected properties of a system. To express such requirements, we define a logic that extends μ-calculus to our coalgebraic definition of systems. We establish an important property of this logic: adequacy.

In this paper, we pursue our works on generic modeling and testing of component-based systems. Here, we extend our conformance testing theory to the testing of component-based systems. We first show that testing a global system can be done by testing its components thanks to the projection of global behaviors onto local ones. Secondly, based on our projection techniques, we define a framework to build adequate test purposes automatically for testing components in the context of the global system where they are plugged in. The basic idea is to identify from any trace try of the global system, the trace of any component involved in tr. Those projected traces can be then seen as test cases that should be tested on individual components.

This paper presents a symbolic execution framework devoted to system models, recursively defined by interconnecting component models. Our concern is to allow one to explicitly define interaction rules between components, while taking into account those rules at the symbolic execution phase. The paper introduces a small set of primitives dedicated to this purpose, together with their associated symbolic execution rules.

Reactive systems are often described by interconnecting sub-components along architectural connectors defining communication policies. Generally, such global systems may exhibit properties, often called "emergent properties", that cannot be anticipated just from a complete knowledge of components. These emergent properties are twofold: (1) the global system can question properties attached to components; (2) some global properties cannot be inferred only from a complete knowledge of components, but for being inferred, need the knowledge of cooperation mechanisms between components. In practice, properties of the second form combine knowledge inherited from components. Thus, they are often defined in a richer language than the ones associated to each component and the presence of such emergent properties is quite natural. In this paper, we restrict ourselves to reactive systems described by means of transition systems as components and of the usual synchronous product as architectural connector and whose behavior is expressed by logical properties over a modal first-order logic. In this framework, we propose to study complexity of reactive systems through this notion of emergent properties and we will give some conditions to guarantee when a system has not emergent properties of the first form.

A mathematical denotation is proposed for the notion of complex software systems whose behavior is specified by rigorous formalisms. Complex systems are described in a recursive way as an interconnection of subsystems by means of architectural connectors. In order to consider the largest family of specification formalisms and architectural connectors, this denotation is essentially formalism, specification and connector independent. For this, we build our denotation on Goguen's institution theory. We then denote in this abstract framework, complexity by the notion of property emergence.

In the framework of functional testing from algebraic specifications, the strategy of test selection which has been widely and efficiently applied is based on axiom unfolding. In this paper, we propose to extend this selection strategy to a modal formalism used to specify dynamic and reactive systems. Such a work is then a first step to tackle testing of such systems more abstractly than most of the works dealing with what is called conformance testing. We get a higher level of abstraction since our specifications account for what is usually called underspecification, i.e. they do not denote a unique model but a class of models. Hence, the testing process can be applied at every design level.

In this paper, we present a code generator transforming a class of CASL specifications into O'Caml programs. This code generator is dedicated to rapid prototyping of CASL specifications especially in the area of geometric modeling where algebraic formalisms have been used since the last decade. A large class of constructive equational specifications is handled by this generator while insuring the correctness of generated O'Caml programs. In particular, CASL specifications with many interpretation models (i.e. incomplete) are automatically supplemented in order to produce a program that implements one of them. Underlying properties, such as termination, completeness and confluence hold when equations satisfy some syntactic criteria given in the paper.

In this paper, we present a temporal logic called /spl Fscr/ whose interpretation is over input output symbolic transition systems (IOSTS). IOSTS extend transition systems to communications and data in order to tackle communications with system environment. /spl Fscr/ is then defined as an extension of temporal logic CTL* (a temporal logic which mixes together the features of linear temporal logic (LTL) and computational temporal logic (CTL)). Three basic properties are established on /spl Fscr/: adequacy and preservation of properties along synchronized product and IOSTS refinement.

In this paper, we investigate the formal specification of reactive systems described in an object-oriented style. We define a formalism, called ÉTOILE1-specifications, to deal with concurrent (active) object systems, and propose to extend algebraic approaches to dynamic and concurrent aspects by considering implicit states and implicit transitions, respectively. ÉTOILE-specifications emphasize systems composed of object types. Consequently, the ÉTOILE-formalism is split into two sub-formalisms. The first one enables us to specify the behaviour of object types. Then, it is extended from object types to systems by adding new requirements, mainly to describe the underlying architectural aspects of the system under specification (i.e. relationships between objects). The complexity of real systems results in the definition of formal means to manage their size. To deal with this issue, we propose a refinement of object type specifications by systems in the framework of ÉTOILE-specifications, which enables one to build his(her) specification in an incremental way.

We present an institution of feature logics which generalises our earlier approach (2001) and define a refinement theory to deal with the complexity of feature interactions in this generic framework, which is one of the main problems encountered when dealing with feature interaction detection. The study of interactions through implementation techniques is still an open problem. The authors furnish answers to encounter this purpose in a logic-independent framework, using algebraic refinement techniques.