A formal model of real-time program compilation

Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code, Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints. (C) 2002 Elsevier Science B.V. All rights reserved.

Qualitative and quantitative formal model-based safety analysis : push the safety button

Magdeburg, Univ., Fak. für Informatik, Diss., 2011

A formal model of the Semantic Web Service Ontology (WSMO)

Semantic Web Service, one of the most significant research areas within the Semantic Web vision, has attracted increasing attention from both the research community and industry. The Web Service Modelling Ontology (WSMO) has been proposed as an enabling framework for the total/partial automation of the tasks (e.g., discovery, selection, composition, mediation, execution, monitoring, etc.) involved in both intra- and inter-enterprise integration of Web services. To support the standardisation and tool support of WSMO, a formal model of the language is highly desirable. As several variants of WSMO have been proposed by the WSMO community, which are still under development, the syntax and semantics of WSMO should be formally defined to facilitate easy reuse and future development. In this paper, we present a formal Object-Z formal model of WSMO, where different aspects of the language have been precisely defined within one unified framework. This model not only provides a formal unambiguous model which can be used to develop tools and facilitate future development, but as demonstrated in this paper, can be used to identify and eliminate errors present in existing documentation.

Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.

Policy Making in Divided Government. A Pivotal Actors Model with Party Discipline.

This article presents a formal model of policy decision-making in an institutional framework of separation of powers in which the main actors are pivotal political parties with voting discipline. The basic model previously developed from pivotal politics theory for the analysis of the United States lawmaking is here modified to account for policy outcomes and institutional performances in other presidential regimes, especially in Latin America. Legislators' party indiscipline at voting and multi-partism appear as favorable conditions to reduce the size of the equilibrium set containing collectively inefficient outcomes, while a two-party system with strong party discipline is most prone to produce 'gridlock', that is, stability of socially inefficient policies. The article provides a framework for analysis which can induce significant revisions of empirical data, especially regarding the effects of situations of (newly defined) unified and divided government, different decision rules, the number of parties and their discipline. These implications should be testable and may inspire future analytical and empirical work.

Policy making in divided government. A pivotal actors model with party discipline

This article presents a formal model of policy decision-making in an institutional framework of separation of powers in which the main actors are pivotal political parties with voting discipline. The basic model previously developed from pivotal politics theory for the analysis of the United States lawmaking is here modified to account for policy outcomes and institutional performances in other presidential regimes, especially in Latin America. Legislators' party indiscipline at voting and multi-partism appear as favorable conditions to reduce the size of the equilibrium set containing collectively inefficient outcomes, while a two-party system with strong party discipline is most prone to produce 'gridlock', that is, stability of socially inefficient policies. The article provides a framework for analysis which can induce significant revisions of empirical data, especially regarding the effects of situations of (newly defined) unified and divided government, different decision rules, the number of parties and their discipline. These implications should be testable and may inspire future analytical and empirical work.

Ateliê caderneta de cromos : estudo sobre a relação de uma prática artística visual não formal e inclusão

Esta investigação teve como objeto de estudo o Ateliê Caderneta de Cromos, do projeto Geração Cool, fruto de uma parceria entre várias instituições do concelho de Almada. Trata--se de um projeto de desenvolvimento social comunitário, multicultural, associado a uma escola. Através de um estudo de caso, pretendeu analisar-se, criticamente, um modelo não formal de práticas ligadas às artes visuais, vocacionado para jovens em risco e mostrar como as aprendizagens desenvolvidas num ateliê de artes visuais contribuem para o processo de inclusão desses jovens. Desenvolveu-se um quadro teórico abrangente, no sentido de sustentar as perguntas iniciais, referenciando questões consideradas pertinentes tais como: visões contemporâneas das realidades multiculturais das periferias urbanas; perspetivas pós-modernistas de ensino artístico, defensoras de uma construção cognitiva; ação dos projetos artísticos de desenvolvimento social e ainda, a importância ética e social dos currículos artísticos atuais. Tendo como referência a hipótese de antagonismo e/ou complementaridade entre o ato pedagógico não formal e o institucional, o estudo procurou estabelecer uma relação entre essa prática e a inclusão, ao identificar e desmontar um roteiro estratégico de aprendizagens. O ato pedagógico no Ateliê mostrou potenciar uma aprendizagem construtiva nas respostas produzidas, sendo também significativa pelo caráter experiencial vivido e cognitiva no sentido em que determina a construção de um significado, assumido como a própria assunção identitária.

Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry

Elementos estruturais de um modelo formal dos esportes coletivos de invasão

O desenvolvimento de um modelo formal da estratégia e da dinâmica do jogo constitui uma contribuição científica original no contexto dos esportes coletivos de invasão. O procedimento construtivo de uma estratégia definido no modelo é composto de cinco conjuntos de elementos ordenados em níveis hierárquicos, que suportam o desenho de estratégias capazes de orientar adequadamente uma equipe em um jogo. Uma vez definido o modelo da estratégia, a formalização da dinâmica do jogo permite sua contextualização no momento de sua aplicação para orientar os jogadores no confronto. O jogo teve sua estrutura decomposta e suas propriedades dinâmicas fundamentais foram definidas. Dessa forma, a modelagem da dinâmica da oposição e da estratégia se complementam, pois definem os momentos nos quais a informação estratégica é utilizada pelos jogadores. A estrutura formal apresentada inaugura uma linha de pesquisa que poderá contribuir para limitar a subjetividade na definição dos critérios de análise de futuros desenhos experimentais, levando à interpretações e comparações mais acuradas dos resultados dos estudos.

An Economic Model of Fair Use

The doctrine of fair use allows limited copying of creative works based on the rationale that copyright holders would consent to such uses if bargaining were possible. This paper develops a formal model of fair use in an effort to derive the efficient legal standard for applying the doctrine. The model interprets copies and originals as differentiated products and defines fair use as a threshold separating permissible copying from infringement. The analysis highlights the role of technology in shaping the efficient standard. Discussion of several key cases illustrates the applicability of the model.

Garantía de calidad en Educación Virtual No Formal para Pueblos Indígenas

Este trabajo de investigación presenta un modelo de garantía de calidad en educación Alternativa en modalidad virtual para Pueblos Indígenas del departamento de La Paz, Bolivia. Se plantea el modelo teórico constituido por componentes que emergen de la problemática enunciada, complementado con un análisis comparativo de modelos de calidad en educación virtual y la selección de variables e indicadores. Se da también una descripción del modelo causal explicativo inicial, todo esto utilizando elementos adecuados a las características de Pueblos indígenas del Dpto. de La Paz. Más adelante, se detalla la experiencia de capacitación en TIC’s a dos poblaciones indígenas aplicando el modelo planteado, lo que ha permitido hacer una validación empírica de este. Asimismo, se da a conocer los resultados que arrojaron las encuestas de calidad provenientes de la aplicación del modelo y el llenado correspondiente de las mismas. A partir de estos datos se ha realizado los análisis estadísticos pertinentes para una validación formal del modelo, estructurando una base de datos con la que se logra validar el modelo a través del análisis confirmatorio que conduce a verificar el ajuste de los datos muestrales con el modelo propuesto. ABSTRACT This research presents a model of quality assurance in Alternative education in virtual mode for indigenous communities in the department of La Paz, Bolivia. The theoretical model consisting of components that emerge from the problem expressed, supplemented by a comparative analysis of quality models in virtual education and the selection of variables and indicators arise. It also gives a description of the initial causal explanatory model, all using suited to the characteristics of indigenous communities in the Department of La Paz. Later, the experience of ICT training in two indigenous peoples applying the detailed proposed model, which has allowed for an empirical validation of this. It also discloses the results yielded quality surveys from the application of the model and the corresponding filling them. From these data it was performed statistical analysis relevant to a formal model validation, structuring a database with that achieved validate the model through confirmatory analysis leading to check the setting of the sample data with the model proposed.

A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.