Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

A formal methodology for the verification of concurrent systems

There is an increasing emphasis on the use of software to control safety critical plants for a wide area of applications. The importance of ensuring the correct operation of such potentially hazardous systems points to an emphasis on the verification of the system relative to a suitably secure specification. However, the process of verification is often made more complex by the concurrency and real-time considerations which are inherent in many applications. A response to this is the use of formal methods for the specification and verification of safety critical control systems. These provide a mathematical representation of a system which permits reasoning about its properties. This thesis investigates the use of the formal method Communicating Sequential Processes (CSP) for the verification of a safety critical control application. CSP is a discrete event based process algebra which has a compositional axiomatic semantics that supports verification by formal proof. The application is an industrial case study which concerns the concurrent control of a real-time high speed mechanism. It is seen from the case study that the axiomatic verification method employed is complex. It requires the user to have a relatively comprehensive understanding of the nature of the proof system and the application. By making a series of observations the thesis notes that CSP possesses the scope to support a more procedural approach to verification in the form of testing. This thesis investigates the technique of testing and proposes the method of Ideal Test Sets. By exploiting the underlying structure of the CSP semantic model it is shown that for certain processes and specifications the obligation of verification can be reduced to that of testing the specification over a finite subset of the behaviours of the process.

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.

Modeling of Distributed Control Systems in Intelligent Building based on Colored Petri Nets

Distributed control systems consist of sensors, actuators and controllers, interconnected by communication networks and are characterized by a high number of concurrent process. This work presents a proposal for a procedure to model and analyze communication networks for distributed control systems in intelligent building. The approach considered for this purpose is based on the characterization of the control system as a discrete event system and application of coloured Petri net as a formal method for specification, analysis and verification of control solutions. With this approach, we develop the models that compose the communication networks for the control systems of intelligent building, which are considered the relationships between the various buildings systems. This procedure provides a structured development of models, facilitating the process of specifying the control algorithm. An application example is presented in order to illustrate the main features of this approach.

Development of Control Systems for Safety Instrumented Systems

Safety Instrumented Systems (SIS) are designed to prevent and / or mitigate accidents, avoiding undesirable high potential risk scenarios, assuring protection of people`s health, protecting the environment and saving costs of industrial equipment. The design of these systems require formal methods for ensuring the safety requirements, but according material published in this area, has not identified a consolidated procedure to match the task. This sense, this article introduces a formal method for diagnosis and treatment of critical faults based on Bayesian network (BN) and Petri net (PN). This approach considers diagnosis and treatment for each safety instrumented function (SIF) including hazard and operability (HAZOP) study in the equipment or system under control. It also uses BN and Behavioral Petri net (BPN) for diagnoses and decision-making and the PN for the synthesis, modeling and control to be implemented by Safety Programmable Logic Controller (PLC). An application example considering the diagnosis and treatment of critical faults is presented and illustrates the methodology proposed.

Assessment of psychosocial adjustment in patients with temporal lobe epilepsy using a standard measure

Despite the growing evidence of poor psychosocial adjustment, at present there is no formal method of assessment of social adjustment in patients with temporal lobe epilepsy (TLE). First, we assessed social adjustment in patients with TLE using a self-report questionnaire and compared the results with those from quality-of-life (QOL) scales. Second, we verified the influence of cognitive performance and clinical variables of epilepsy on social adjustment and QOL We evaluated 35 people with TLE and 38 healthy controls. Patients had worse social adjustment, and it was correlated with worse perception of cognitive function. Attention and verbal memory dysfunctions were negatively correlated with social adjustment. However, there was no significant correlation between cognitive performance and QOL Regarding clinical variables, persons with left TLE showed worse social adjustment and patients with frequent seizures showed worse QOL These findings indicate the relevance of evaluating social adjustment and emphasize the importance of cognitive rehabilitation to improved social adjustment. (c) 2010 Elsevier Inc. All rights reserved.

Mapping the diagnosis axis of an interface terminology to the NANDA International Taxonomy

Background: Nursing terminologies are designed to support nursing practice but, as with any other clinical tool, they should be evaluated. Cross-mapping is a formal method for examining the validity of the existing controlled vocabularies. Objectives: The study aims to assess the inclusiveness and expressiveness of the nursing diagnosis axis of a newly implemented interface terminology by cross-mapping with the NANDA-I taxonomy. Design/Methods: The study applied a descriptive design, using a cross-sectional, bidirectional mapping strategy. The sample included 728 concepts from both vocabularies. Concept cross-mapping was carried out to identify one-to-one, negative, and hierarchical connections. The analysis was conducted using descriptive statistics. Results: Agreement of the raters" mapping achieved 97%. More than 60% of the nursing diagnosis concepts in the NANDA-I taxonomy were mapped to concepts in the diagnosis axis of the new interface terminology; 71.1% were reversely mapped. Conclusions: Main results for outcome measures suggest that the diagnosis axis of this interface terminology meets the validity criterion of cross-mapping when mapped from and to the NANDA-I taxonomy.

A Type-Preserving Compiler from System F to Typed Assembly Language

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code

Plan exportador software de encriptación y firma digital de documentos altamente sensibles

Este plan exportador proyectado a un plazo de 3 años, servirá a ITAC IT APPLICATIONS CONSULTING S.A. para direccionar sus actividades en el mercado internacional para los años 2009, 2010, 2011. La prioridad de los 2 primeros años será el mejoramiento interno de la empresa, que será la aplicación de estrategias en diferentes campos como: capital humano, capital intelectual, capital cultural, crecimiento económico, estrategia comercial en el área internacional, construcción de capital financiero para la generación de ingresos. Para tener participación en mercados internacionales, mostrar su potencial exportador y lograr las expectativas de crecimiento de las ventas independientes a las obtenidas en el marcado local; pretende empezar en el año 2009, en el mercado Peruano con exportaciones por $36.000 USD correspondiente a 30 unidades, aumentando a $ 72000 USD con 60 unidades en el 2010 y $ 108000 USD y 90 unidades en el 2011. El Servicio a exportar fue “SecureFile” a partir del cual se definieron factores de éxito como lo son las ventajas competitivas del producto en sí mismo enumeradas a continuación: 1) Precio muy competitivo en el mercado, 2) Automatización del proceso de intercambio de información, 3) Software basado en estándares, 4) Se ejecuta en cualquier sistema operativo. A su vez se realizaron consultorías donde se diagnosticó todas las áreas de la empresa arrojando algunos resultados: La estructura organizacional esta bien definida, pero por su crecimiento y necesidad de incluir nuevo personal, no hay claridad en las funciones dentro del organigrama y depende totalmente de la dirección general. Por esto la gerencia debe estructurar mejor los departamentos comerciales creando nuevos cargos de acuerdo al proceso de internacionalización. Las políticas de personal se trabajan de manera informal con criterios validos para promover trabajadores (mérito, antigüedad, etc.), se realizan actualizaciones Tecnológicas mensuales, reconocimiento y participación en la empresa a sus funcionarios, excelentes relaciones personales que permiten hacer evaluaciones de desempeño acorde a las metas, gran variedad de motivación y responsabilidad social encaminada a los niños de bajos recursos. Aunque se debe crear un área de gestión humana y definir la frecuencia de las capacitaciones. Los ingresos son provenientes de la prestación de servicios de IT con incrementando de 256% durante los tres años anteriores para obtener $ 2`032.784.683 millones de pesos en el 2007. El nivel de endeudamiento también ha ido en aumento, por la necesidad de capacidad instalada, contrataciones de personal, el cumplimiento de requisitos del mercado y la necesidad generar buena imagen crediticia con entidades financieras. Cuenta con un musculo financiero para respaldar sus obligaciones inmediatas con $4,42 por $1 comprometido en el 2007 a pesar de ser el año con mayor nivel de endeudamiento arrojando pasivos corrientes por $127.715.281,37. Los cuatro socios cuentan con un comportamiento de 164,67% (2006) y 132,97% (2007) de rendimiento de sobre la inversión antes de impuestos. Para este año más del 95% de su información financiera y contable se maneja de manera sistematizada. El área Financiera de la empresa no es la más débil, pero no existe un departamento financiero con un solo responsable a la cabeza, por esto deben destinar un área separada de la administrativa con un asesor financiero que tenga disponibilidad de 100%. En el caso particular del proyecto de exportación los costos de producción se centran en SecureFile versión 3.0 que no representa costos marginales, ya que la replica de este software puede hacerse cuantas veces sea requerido sin afectar en ninguna proporción los costos. La empresa no utiliza un método formal para calcular sus costos de operación y desarrollo de programas. Pero ha desarrollado un sistema de evaluación de costos en tablas de Excel que de manera organizada logran un costeo acorde a sus necesidades específicas. Para la selección de los países: objetivo, alterno y contingente; se realizó una matriz de Selección de 6 países basados en la exigencia gubernamental en términos de seguridad de la información vía internet, y la percepción de los empresarios, competencia y otros factores económicos; arrojando como resultado a Perú, Costa Rica y México.

A mission control system for an autonomous underwater vehicle

The presented work focuses on the theoretical and practical aspects concerning the design and development of a formal method to build a mission control system for autonomous underwater vehicles bringing systematic design principles for the formal description of missions using Petri nets. The proposed methodology compounds Petri net building blocks within it to de_ne a mission plan for which it is proved that formal properties, such as reachability and reusability, hold as long as these same properties are also guaranteed by each Petri net building block. To simplify the de_nition of these Petri net blocks as well as their composition, a high level language called Mission Control Language has been developed. Moreover, a methodology to ensure coordination constraints for teams of multiple robots as well as the de_nition of an interface between the proposed system and an on-board planner able to plan/replan sequences of prede_ned mission plans is included as well. Results of experiments with several real underwater vehicles and simulations involving an autonomous surface craft and an autonomous underwater vehicles are presented to show the system's capabilities.

A Compositional Semantics of UML-RSDS

This paper provides a semantics for the UML-RSDS (Reactive System Development Support) subset of UML, using the real-time action logic (RAL) formalism. We show how this semantics can be used to resolve some ambiguities and omissions in UML semantics, and to support reasoning about specifications using the B formal method and tools. We use `semantic profiles' to provide precise semantics for different semantic variation points of UML. We also show how RAL can be used to give a semantics to notations for real-time specification in UML. Unlike other approaches to UML semantics, which concentrate on the class diagram notation, our semantic representation has behaviour as a central element, and can be used to define semantics for use cases, state machines and interactions, in addition to class diagrams.

Uma arquitetura para sistemas supervisórios industriais e sua aplicação em processos de elevação artificial de petróleo

The using of supervision systems has become more and more essential in accessing, managing and obtaining data of industrial processes, because of constant and frequent developments in industrial automation. These supervisory systems (SCADA) have been widely used in many industrial environments to store process data and to control the processes in accordance with some adopted strategy. The SCADA s control hardware is the set of equipments that execute this work. The SCADA s supervision software accesses process data through the control hardware and shows them to the users. Currently, many industrial systems adopt supervision softwares developed by the same manufacturer of the control hardware. Usually, these softwares cannot be used with other equipments made by distinct manufacturers. This work proposes an approach for developing supervisory systems able to access process information through different control hardwares. An architecture for supervisory systems is first defined, in order to guarantee efficiency in communication and data exchange. Then, the architecture is applied in a supervisory system to monitor oil wells that use distinct control hardwares. The implementation was modeled and verified by using the formal method of the Petri networks. Finally, experimental results are presented to demonstrate the applicability of the proposed solution

BTS:uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes

The component-based development of systems revolutionized the software development process, facilitating the maintenance, providing more confiability and reuse. Nevertheless, even with all the advantages of the development of components, their composition is an important concern. The verification through informal tests is not enough to achieve a safe composition, because they are not based on formal semantic models with which we are able to describe precisally a system s behaviour. In this context, formal methods provide ways to accurately specify systems through mathematical notations providing, among other benefits, more safety. The formal method CSP enables the specification of concurrent systems and verification of properties intrinsic to them, as well as the refinement among different models. Some approaches apply constraints using CSP, to check the behavior of composition between components, assisting in the verification of those components in advance. Hence, aiming to assist this process, considering that the software market increasingly requires more automation, reducing work and providing agility in business, this work presents a tool that automatizes the verification of composition among components, in which all complexity of formal language is kept hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport) helps to create and compose components, predicting, in advance, undesirable behaviors in the system, such as deadlocks