Search

It can be argued that participating in free/libre open source software (FLOSS) projects can have a positive effect in the contributor's learning process. The need to interact with other contributors, to read other people's code, write documentation, or use different tools, can motivate and implicitly foster learning. In order to validate this statement we design an appropriate questionnaire asking FLOSS contributors about their experience in FLOSS projects. In this paper, we illustrate how this questionnaire was designed and what we expect to learn from the answers. We conclude the paper with a preview of the results from three cases studies., (undefined)

Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, refining sentential into equational specifications and the latter into modal ones., The authors express their gratitude to the anonymous referees who raised a number of pertinent questions entailing a more precise characterisation of the paper's contributions and a clarification of their scope. This work was funded by HRDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-028923 (Nasoni) and the project PEst-C/MAT/UI4106/2011 with COMPETE number FCOMP-01-0124-FEDER-022690 (CIDMA-UA). The first author also acknowledges the financial assistance by the projects GetFun, reference FP7-PEOPLE-2012-IRSES, and NOCIONES IDE COMPLETUD, reference FFI2009-09345 (MICINN - Spain). A. Madeira was supported by the FCT within the project NORTE-01-0124-FEDER-000060.

This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics.

Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. ALLOY is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to other tools in order to meet such challenges. This paper’s proposal, however, is not establishing a link from ALLOY to another single tool, but rather to “plunge” it into the HETS network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. Semantical foundations for this integration are discussed in detail., FCT

This paper extends the authors’ previous work on a formal approach to the specification of reconfigurable systems in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves vary. In other words, interfaces may evolve, as well., FCT

This paper discusses FLOSS communities as a prime example of learning networks, i.e. informal, interconnected sets of individuals mutually supporting shared knowledge acquisition and committed to self-defined goals. In particular, it addresses how the incorporation of a web-based, certification platform for Free / Libre Open Source Software in community culture and practice may increase the community impact both as learning network and open, high-quality software producer, FCT

Software QoS properties, such as response time, availability, bandwidth requirement, memory usage, among many others, play a major role in the processes of selecting and composing software components. This paper extends a component calculus to deal, in an effective way, with them. The calculus models components as generalised Mealy machines, i.e., state-based entities interacting along their life time through well defined interfaces of observers and actions. QoS is introduced through an algebraic structure specifying the relevant QoS domain and how its values are composed under different disciplines. A major effect of introducing QoS-awareness is that a number of equivalences holding in the plain calculus become refinement laws. The paper also introduces a prototyper for the calculus developed as a ‘proof-of-concept’ implementation., FCT -Fuel Cell Technologies Program(FCOMP-01-0124-FEDER-020537)

We present an approach to analyse the application of tactics in architectural patterns. We define and illustrate the approach by resorting to Archery, a language for specifying, analysing and verifying architectural patterns. The approach consists of characterising the design principles of an architectural pattern as constraints, expressed in the language, and then, establishing a refinement relation based on their satisfaction. The application of tactics preserving refinement preserves the original design principles expressed themselves as constraints for the architectural pattern. The paper’s focus on fault-tolerance tactics, and identifies a set of requirements for a semantic framework characterising them. Model transformations to represent their application are discussed and illustrated through two case studies., FCT

This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper’s main contribution is to pro- vide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them., Fundação para a Ciência e a Tecnologia (FCT)

Extended version including all proofs, Modal logics are successfully used as specification logics for reactive systems. However, they are not expressive enough to refer to individual states and reason about the local behaviour of such systems. This limitation is overcome in hybrid logics which introduce special symbols for naming states in models. Actually, hybrid logics have recently regained interest, resulting in a number of new results and techniques as well as applications to software specification. In this context, the first contribution of this paper is an attempt to ‘universalize’ the hybridization idea. Following the lines of [DS07], where a method to modalize arbitrary institutions is presented, the paper introduces a method to hybridize logics at the same institution-independent level. The method extends arbitrary institutions with Kripke semantics (for multi-modalities with arbitrary arities) and hybrid features. This paves the ground for a general result: any encoding (expressed as comorphism) from an arbitrary institution to first order logic (FOL) deter- mines a comorphism from its hybridization to FOL. This second contribution opens the possibility of effective tool support to specification languages based upon logics with hybrid features., Fundação para a Ciência e a Tecnologia (FCT)

Software connectors are external coordination devices which ensure the flow of data and enforce synchronization constraints within a component’s network. The specification of software connectors through which context dependent behaviour is correctly propagated remains an open, non trivial issue in their semantics. This paper, building on previous work by the authors, revisits this problem and introduces a model in which context awareness is suitably handled.

Component’s QoS constraints cannot be ignored when composing them to build reliable loosely-coupled, distributed systems. Therefore they should be explicitly taken into account in any formal model for component-based development. Such is the purpose of this paper: to extend a calculus of component composition to deal, in an effective way, with QoS constraints. Particular emphasis is put on how the laws that govern composition can be derived, in a calculational, pointfree style, in this new model.

Refinement by interpretation replaces signature morphisms by logic interpretations as a means to translate specifications and witness refinements. The approach was recently introduced by the authors [13] in the context of equational specifications, in order to capture a number of relevant transformations in software design, reuse and adaptation. This paper goes a step forward and discusses the generalization of this idea to deductive systems of arbitrary dimension. This makes possible, for example, to refine sentential into equational specifications and the latter into modal ones. Moreover, the restriction to logics with finitary consequence relations is dropped which results in increased flexibility along the software development process., UA -Universidade de Aveiro(SFRH/BDE/33650/2009)

Traditional notions of refinement of algebraic specifications, based on signature morphisms, are often too rigid to capture a number of relevant transformations in the context of software design, reuse and adaptation. This paper proposes an alternative notion of specification refinement, building on recent work on logic interpretation. The concept is discussed, its theory partially developed, its use illustrated through a number of examples.

More and more current software systems rely on non trivial coordination logic for combining autonomous services typically running on different platforms and often owned by different organizations. Often, however, coordination data is deeply entangled in the code and, therefore, difficult to isolate and analyse separately. CoordInspector is a software tool which combines slicing and program analysis techniques to isolate all coordination elements from the source code of an existing application. Such a reverse engineering process provides a clear view of the actually invoked services as well as of the orchestration patterns which bind them together. The tool analyses Common Intermediate Language (CIL) code, the native language of Microsoft .Net framework. Therefore, the scope of application of CoordInspector is quite large: potentially any piece of code developed in any of the programming languages which compiles to the .Net framework. The tool generates graphical representations of the coordination layer together and identifies the underlying business process orchestrations, rendering them as Orc specifications.

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular, it allows for reasoning about confinement in object-oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

Although increasingly popular, Model Driven Architecture (MDA)still lacks suitable formal foundations on top of which rigorousmethodologies for the description, analysis and transformation ofmodels could be built. This paper aims to contribute in thisdirection: building on previous work by the authors on coalgebraicrefinement for software components and architectures, it discussesrefactoring of models within a coalgebraic semantic framework. Architectures are defined through aggregation based on a coalgebraic semantics for (subsets of)UML. On the other hand, such aggregations, no matter how large and complex they are, can always be dealt with ascoalgebras themselves. This paves the way to a discipline ofmodels' transformations which, being invariant under either behavioural equivalenceor refinement, are able to formally capture a large number of refactoring patterns. The main ideas underlying this research are presented through a detailed example in the context of refactoring of UML class diagrams.

When modelling complex interactive systems, traditional interactor-based approaches suffer from lack of expressiveness regarding the composition of the different interactors present in the user interface model into a coherent system. In this paper we investigate an alternative approach to the composition of interactors for the specification of complex interactive systems which is based on the coordination paradigm. We layout the fundations for the work and present an illustrative example. Lines for future work are identified, Fundação para a Ciência e a Tecnologia (FCT) Fundo Europeu de Desenvolvimento Regional (FEDER)

In a broad sense, computing is an area of knowledge from which a popular and effective technology emerged long before a solid, specific, scientific methodology, let alone formal foundations, had been put forward. This might explain some of the weaknesses in the software industry, on the one hand, as well as an excessively technology-oriented view which dominates computer science training at pre-university and even undergraduate teaching, on the other. Modelling, understood as the ability to choose the right abstractions for a problem domain, is consensually recognised as essential for the development of true engineering skills in this area, as it is in all other engineering disciplines. But, how can the basic problem-solving strategy, one gets used to from school physics: understand the problem, build a mathematical model, reason within the model, calculate a solution, be taken (and taught) as the standard way of dealing with software design problems? This paper addresses this question, illustrating and discussing the interplay between modelling and reasoning.

This paper presents a general model for the analysis of time-delay contributions due to right half plane (RHP) zeros in circuit's transfer functions. The presence of these RHP zeros is in general associated to Miller capacitances. These can be explored as a means of implementation of delay elements. A general discussion on the usage of these RHP zeros as means of designing usable delay cells is addressed, including several parasitic effects that may arise in practical implementations. The model is then verified recurring to simulation experiments.

Delayed-feedback amplifiers are composed of, a forward gain amplifier, a feedback network and a time-delay element. Recently published results claim the possibility of bandwidth enhancement for this type of systems, simply by a judicious choice of loop-gain, open loop poles and the net time-delay. This paper describes the design steps for a shunt-shunt feedback amplifier with an active delay on the feedback loop. The designed circuit was optimized for Free-Space Optical (FSO) line-of-sight receivers. Achieved results show that the inclusion of the active delay, improve bandwidth in a maximum of 60%. A maximum of 1.5 THzOmega GBW (11 kOmega transimpedance gain) was achieved with a photodiode having intrinsic capacitance of 100 pF.

This paper introduces a generic semantic framework for component-based development, expressed in the unified modelling language UML. The principles of a coalgebraic semantics for class, object and statechart diagrams as well as for use cases, are developed. It is also discussed how to formalize the refinement steps in the development process based upon a suitable notion of behavior refinement. In this way, a formal basis for component-based development in UML is studied, which allows the construction of more complex and specific systems from independent components., FCT -Fuel Cell Technologies Program(POSI/ICHS/44304/2002)

Delays in real systems can be of two types: i) intrinsic delays - due to the physical principles of operation of each electronic device; ii) designed delays - due to extra circuits used to add the desired delay. Previous work established the possibility of achieving bandwidth improvements using small delays inside the feedback loop of feedback amplifiers. The modeling approach followed on these contributions used only one designed delay element. The bandwidth reduction effect due to intrinsic delays was not considered on these contributions. This paper extends the concept to the general case of feedback amplifiers that incorporates delays of both types. An experimental demonstration using a simple 0.35μm BiCMOS transimpedance amplifier further confirms the proposed model. © 2006 IEEE.