Formal methods for the development and verification of autonomic IT systems

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach. © 2012, IGI Global.

Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Learning Behind Bars: Exploring Prison Educators’ Facilitation of Inmates’ Self-directed Learning through Garrison’s Model

Formal education programs in prisons have had success in reducing recidivism, but the introduction of informal learning can have additional benefits and longer lasting effects. This paper addresses recidivism and its effects on inmates and society at large and how prison educators can facilitate self-directed learning in prisons through Garrison’s model.

Innovating from the War Economy: Formal, Informal, and Illicit Economic Activities of the Military in Colombia

Over the last decade, the Colombian military has successfully rolled back insurgent groups, cleared and secured conflict zones, and enabled the extraction of oil and other key commodity exports. As a result, official policies of both the Uribe and Santos governments have promoted the armed forces to participate to an unprecedented extent in economic activities intended to consolidate the gains of the 2000s. These include formal involvement in the economy, streamlined in a consortium of military enterprises and social foundations that are intended to put the Colombian defense sector “on the map” nationally and internationally, and informal involvement expanded mainly through new civic action development projects intended to consolidate the security gains of the 2000s. However, failure to roll back paramilitary groups other than through the voluntary amnesty program of 2005 has facilitated the persistence of illicit collusion by military forces with reconstituted “neoparamilitary” drug trafficking groups. It is therefore crucially important to enhance oversight mechanisms and create substantial penalties for collusion with illegal armed groups. This is particularly important if Colombia intends to continue its new practice of exporting its security model to other countries in the region. The Santos government has initiated several promising reforms to enhance state capacity, institutional transparence, and accountability of public officials to the rule of law, which are crucial to locking in security gains and revitalizing democratic politics. Efforts to diminish opportunities for illicit association between the armed forces and criminal groups should complement that agenda, including the following: Champion breaking existing ties between the military and paramilitary successor groups through creative policies involving a mixture of punishments and rewards directed at the military; Investigation and extradition proceedings of drug traffickers, probe all possible ties, including as a matter of course the possibility of Colombian military collaboration. Doing so rigorously may have an important effect deterring military collusion with criminal groups. Establish and enforce zero-tolerance policies at all military ranks regarding collusion with criminal groups; Reward military units that are effective and also avoid corruption and criminal ties by providing them with enhanced resources and recognition; Rely on the military for civic action and development assistance as minimally as possible in order to build long-term civilian public sector capacity and to reduce opportunities for routine exposure of military forces to criminal groups circulating in local populations.

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

The development of a semantic model for the interpretation of mathematics including the use of technology

The semantic model developed in this research was in response to the difficulty a group of mathematics learners had with conventional mathematical language and their interpretation of mathematical constructs. In order to develop the model ideas from linguistics, psycholinguistics, cognitive psychology, formal languages and natural language processing were investigated. This investigation led to the identification of four main processes: the parsing process, syntactic processing, semantic processing and conceptual processing. The model showed the complex interdependency between these four processes and provided a theoretical framework in which the behaviour of the mathematics learner could be analysed. The model was then extended to include the use of technological artefacts into the learning process. To facilitate this aspect of the research, the theory of instrumentation was incorporated into the semantic model. The conclusion of this research was that although the cognitive processes were interdependent, they could develop at different rates until mastery of a topic was achieved. It also found that the introduction of a technological artefact into the learning environment introduced another layer of complexity, both in terms of the learning process and the underlying relationship between the four cognitive processes.

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Estructura formal, textual y oral del discurso público

Estructura formal, textual y oral del discurso públicoExisten tres competencias comunicativas muy valoradas en la sociedad de la información. Primero, la búsqueda, selección y gestión de grandes cantidades de información. Segundo, la redacción de textos claros, concisos y rigurosos. Y en tercer lugar, la exposición y defensa oral de esta información en un discurso público. Tradicionalmente, los estudios de periodismo han abordado estas competencias de forma independiente. Pero actualmente, instituciones y empresas de ámbitos diferentes demandan un perfil profesional capaz de aplicarlas ante cualquier tipo de información y con objetivos diversos. Se propone un modelo integral en tres niveles estructurales basado en teorías, conceptos y estudios específicos de periodismo, oratoria, retórica… o comunicación, en los últimos años. Este modelo puede contribuir a encauzar las investigaciones de académicos y representa una herramienta de entrenamiento para profesionales.

Settlement Duration and Materiality:Formal Chronological Models for the Development of Barnhouse, a Grooved Ware Settlement in Orkney

Radiocarbon dating and Bayesian chronological modelling, undertaken as part of the investigation by the Times of Their Lives project into the development of Late Neolithic settlement and pottery in Orkney, has provided precise new dating for the Grooved Ware settlement of Barnhouse, excavated in 1985–91. Previous understandings of the site and its pottery are presented. A Bayesian model based on 70 measurements on 62 samples (of which 50 samples are thought to date accurately the deposits from which they were recovered) suggests that the settlement probably began in the later 32nd century cal bc (with Houses 2, 9, 3 and perhaps 5a), possibly as a planned foundation. Structure 8 – a large, monumental structure that differs in character from the houses – was probably built just after the turn of the millennium. Varied house durations and replacements are estimated. House 2 went out of use before the end of the settlement, and Structure 8 was probably the last element to be abandoned, probably during the earlier 29th century cal bc. The Grooved Ware pottery from the site is characterised by small, medium-sized, and large vessels with incised and impressed decoration, including a distinctive, false-relief, wavy-line cordon motif. A considerable degree of consistency is apparent in many aspects of ceramic design and manufacture over the use-life of the settlement, the principal change being the appearance, from c. 3025–2975 cal bc, of large coarse ware vessels with uneven surfaces and thick applied cordons, and of the use of applied dimpled circular pellets. The circumstances of new foundation of settlement in the western part of Mainland are discussed, as well as the maintenance and character of the site. The pottery from the site is among the earliest Grooved Ware so far dated. Its wider connections are noted, as well as the significant implications for our understanding of the timing and circumstances of the emergence of Grooved Ware, and the role of material culture in social strategies.

Definition of Model-based diagnosis problems with Altarica

International audience

TAXONOMY, MORPHOLOGY, AND RNA-SEQ TRANSCRIPTOMICS OF THE CUBOZOAN ALATINA ALATA, AN EMERGING MODEL CNIDARIAN

Cnidarians are often considered simple animals, but the more than 13,000 estimated species (e.g., corals, hydroids and jellyfish) of the early diverging phylum exhibit a broad diversity of forms, functions and behaviors, some of which are demonstrably complex. In particular, cubozoans (box jellyfish) are cnidarians that have evolved a number of distinguishing features. Some cubozoan species possess complex mating behaviors or particularly potent stings, and all possess well-developed light sensation involving image-forming eyes. Like all cnidarians, cubozoans have specialized subcellular structures called nematocysts that are used in prey capture and defense. The objective of this study is to contribute to the development of the box jellyfish Alatina alata as a model cnidarian. This cubozoan species offers numerous advantages for investigating morphological and molecular traits underlying complex processes and coordinated behavior in free-living medusozoans (i.e., jellyfish), and more broadly throughout Metazoa. First, I provide an overview of Cnidaria with an emphasis on the current understanding of genes and proteins implicated in complex biological processes in a few select cnidarians. Second, to further develop resources for A. alata, I provide a formal redescription of this cubozoan and establish a neotype specimen voucher, which serve to stabilize the taxonomy of the species. Third, I generate the first functionally annotated transcriptome of adult and larval A. alata tissue and apply preliminary differential expression analyses to identify candidate genes implicated broadly in biological processes related to prey capture and defense, vision and the phototransduction pathway and sexual reproduction and gametogenesis. Fourth, to better understand venom diversity and mechanisms controlling venom synthesis in A. alata, I use bioinformatics to investigate gene candidates with dual roles in venom and digestion, and review the biology of prey capture and digestion in cubozoans. The morphological and molecular resources presented herein contribute to understanding the evolution of cubozoan characteristics and serve to facilitate further research on this emerging cubozoan model.

Forms of Collaboration in Collaborative Enterprises: An Ontological Model

Part 19: Knowledge Management in Networks

Collaborative Networked Organizations as System of Systems: A Model-Based Engineering Approach

Part 6: Engineering and Implementation of Collaborative Networks