Formal development and quantitative verification of dependable systems

-

Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

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.

Ancient Bronze Horse Muzzles of the Iberian Peninsula

[spa]Los bozales y las muserolas en bronce para caballo constituyen unos excepcionales complementos ecuestres cuyo conocimiento se encuentra disperso en una extensa bibliografía. De muchos ejemplares apenas se ha publicado una breve descripción y nunca hasta el presente han sido objeto de un estudio monográfico, quizás por el desaliento que produce el desconocimiento de su procedencia en unos casos, o la superficial noticia del contexto de aparición en la mayoría de ellos, hecho que ha limitado las consideraciones cronológicas y de asociación. La identificación de nuevos ejemplares inéditos en los museos de Barcelona y Lleida ha animado a los autores a emprender un trabajo que por primera vez reúne y revisa los ejemplares conocidos de la Península Ibérica, para los que se propone una descripción normalizada, una clasificación tipológica y, en determinadas piezas, una sustancial revisión de las escenas decorativas y cronologías comúnmente admitidas. La seriación formal y la propuesta de datación implican la referencia de los ejemlares aparecidos en Grecia e Italia. Esa ampliación espacial conduce a replantear los agentes sociales que pueden estar detrás de la propagación de ese complemento ecuestre hasta la peninsua más occidental del Mediterráneo. [eng] Horse muzzles and Bronze muzzles are unique equestrian tools that have been referred to in scattered accounts throughout history. Nevertheless, the majority of these objects have received short descriptions and an overall study is still missing. The lack of a comprehensive study hinges on the over looked importance of these items and the superficial manner that have characterized their documentation. Both these reasons have limited observations on chronology and archaeological investigation. The recent identification of new unpublished exemplars among the Museums" collections in Barcelona and Lleida has encouraged the authors of this paper to start a new study dedicated to these objects. Starting from a catalogue inclusive of all muzzles and muzzles currently known in the Iberian Peninsula, an attempt will be made to propose an accurate description, typological classification and, for some of the items, a revision of the decorative scenes that have marked their place in bronze horse muzzle and muzzle chronology. The formal development and the chronological framework here proposed refer to those of the exemplars found in Greece and in Italy. The broadening of the geographical area will allow reconsideration of those social phenomena that have in the past determined the diffusion of elements in horse tack throughout most of the western Peninsula in the Mediterranean.

Geração de casos de teste a partir de especificações B

With the increasing complexity of software systems, there is also an increased concern about its faults. These faults can cause financial losses and even loss of life. Therefore, we propose in this paper the minimization of faults in software by using formally specified tests. The combination of testing and formal specifications is gaining strength in searches mainly through the MBT (Model-Based Testing). The development of software from formal specifications, when the whole process of refinement is done rigorously, ensures that what is specified in the application will be implemented. Thus, the implementation generated from these specifications would accurately depict what was specified. But not always the specification is refined to the level of implementation and code generation, and in these cases the tests generated from the specification tend to find fault. Additionally, the generation of so-called "invalid tests", ie tests that exercise the application scenarios that were not addressed in the specification, complements more significantly the formal development process. Therefore, this paper proposes a method for generating tests from B formal specifications. This method was structured in pseudo-code. The method is based on the systematization of the techniques of black box testing of boundary value analysis, equivalence partitioning, as well as the technique of orthogonal pairs. The method was applied to a B specification and B test machines that generate test cases independent of implementation language were generated. Aiming to validate the method, test cases were transformed manually in JUnit test cases and the application, created from the B specification and developed in Java, was tested. Faults were found with the execution of the JUnit test cases

A concepção das crianças e os valores associados à doação de sangue: doadores do futuro

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Against Logically Possible World-Relativized Existence

The thesis that entities exist in, at, or in relation to logically possible worlds is criticized. The suggestion that actually nonexistent fictional characters might nevertheless exist in nonactual merely logically possible worlds runs afoul of the most general transworld identity requirements. An influential philosophical argument for the concept of world-relativized existence is examined in Alvin Plantinga’s formal development and explanation of modal semantic relations. Despite proposing an attractive unified semantics of alethic modality, Plantinga’s argument is rejected on formal grounds as supporting materially false actual existence assertions in the case of actually nonexistent objects in the framework of Plantinga’s own underlying classical predicate-quantificational logic.

La arquitectura de Víctor Eusa

El arquitecto Víctor Eusa (Pamplona, 1894-1990) es la figura central de la arquitectura en Navarra durante la mayor parte del siglo XX. Desde 1920, año en que termina sus estudios en Madrid, hasta 1973, año de su jubilación, produjo centenares de obras y proyectos en esta región española, con esporádicas intervenciones en otras zonas, como las provincias vecinas de Guipúzcoa, Vizcaya y Zaragoza. Su periodo activo coincide con el de la construcción del II Ensanche de Pamplona. La cantidad y calidad de su producción hacen posible establecer una identificación entre la obra de Eusa y la ciudad entonces existente. Sus obras principales son auténticos hitos urbanos que caracterizan el Ensanche. El archivo personal del arquitecto se perdió desgraciadamente en los años setenta del pasado siglo. Este trabajo de investigación ha partido de la recopilación de la documentación gráfica existente en archivos públicos y privados, que ha dado como fruto la catalogación de las obras y proyectos de Víctor Eusa, que constituye el tomo II de la tesis. En el tomo I se analiza la trayectoria del arquitecto y la evolución formal de su lenguaje, a partir de su formación académica y las sucesivas influencias que jalonan sus primeros años de profesión: sus viajes por Europa y Oriente, Otto Wagner y la Sezession vienesa, Perret y el hormigón armado, el Art-Déco y la Exposición de París de 1925, Dudok y la arquitectura holandesa, etc. Todo ello fructifica en una arquitectura expresionista muy personal, basada en la geometría de líneas rectas y quebradas, que combina el ladrillo y el hormigón como sus materiales preferidos. Su madurez se alcanza a finales de los años veinte y se prolonga hasta la guerra civil española. En este periodo se concentran sus obras más conocidas: Casa de Misericordia, Iglesia de los Paúles, Colegio de Escolapios, edificios de viviendas en plaza Príncipe de Viana y calle García Castañón, Seminario, Casino Eslava,… Después del 36, sus responsabilidades públicas sucesivas como arquitecto municipal de Pamplona y como arquitecto provincial de la Diputación Foral de Navarra introducen en su obra una nueva dimensión urbana. ABSTRACT The architect Víctor Eusa (Pamplona, 1894-1990) was the central figure in architecture in Navarra for most of the 20th century. From 1920, when he finished his studies in Madrid, to his retirement in 1973, he was responsible for hundreds of buildings in Navarra, as well as occasional projects in the neighbouring provinces of Guipúzcoa, Vizcaya and Zaragoza. His career as an architect developed in parallel with the second phase of urban expansion in Pamplona. In terms of both quantity and quality, this new district can be seen as an embodiment of Eusa's work, and his most outstanding buildings form the landmarks which give character to this area. Unfortunately, Eusa's personal archive was lost in the 1970s. By collecting and analyzing the graphic information available in public archives, the author of this dissertation was able to compile a catalogue of Eusa's work and projects, which is provided in volume II. Volume I focuses on Eusa's career and the formal development of his language, starting from his academic training and tracing the successive influences that were at work during his early years as an architect: his journeys through Europe and the East, Otto Wagner and the Vienna Secession, Perret and reinforced concrete, Art-Déco and the Paris Exhibition of 1925, Dudok and the Dutch architecture represented in the magazines Wendingen and De Stijl, and many others. All of this came together in Eusa's highly personal expressionist style, based on a geometry of straight and zigzag lines, combining his favourite materials, brick and concrete. His mature period consolidated by end of the 1920s and lasted until the Spanish Civil War. After 1936, Eusa's responsibilities as municipal architect for Pamplona and later as head of architecture for Navarra enabled him to develop his talents in the area of urban design.

Language acquisition during a stay abroad period following formal instruction: temporal effects on oral fluency development

This study investigates the development of fluency in 30 advanced L2 learners of English over a period of 15 months. In order to measure fluency, several temporal variables and hesitation phenomena are analyzed and compared. Oral competence is assessed by means of an oral interview carried out by the learners. Data collection takes place at three different times: before (T1) and after (T2) a six-month period of FI (80 hours) in the home university, and after a three-month SA term (T3). The data is analyzed quantitatively. Developmental gains in fluency are measured for the whole period, adopting a view of complementarity between the two learning contexts. From these results, a group of high fluency speakers is identified. Correlations between fluency gains and individual and contextual variables are executed and a more qualitative analysis is performed for high fluency speakers' performance and behavior. Results show an overall development of students' oral fluency during a period of 15 months favored by the combination of a period of FI at home followed by a 3-months SA.