Formal development and quantitative verification of dependable systems

-

Reusable formal architectures for networked systems

Today's networked systems are becoming increasingly complex and diverse. The current simulation and runtime verification techniques do not provide support for developing such systems efficiently; moreover, the reliability of the simulated/verified systems is not thoroughly ensured. To address these challenges, the use of formal techniques to reason about network system development is growing, while at the same time, the mathematical background necessary for using formal techniques is a barrier for network designers to efficiently employ them. Thus, these techniques are not vastly used for developing networked systems. The objective of this thesis is to propose formal approaches for the development of reliable networked systems, by taking efficiency into account. With respect to reliability, we propose the architectural development of correct-by-construction networked system models. With respect to efficiency, we propose reusable network architectures as well as network development. At the core of our development methodology, we employ the abstraction and refinement techniques for the development and analysis of networked systems. We evaluate our proposal by employing the proposed architectures to a pervasive class of dynamic networks, i.e., wireless sensor network architectures as well as to a pervasive class of static networks, i.e., network-on-chip architectures. The ultimate goal of our research is to put forward the idea of building libraries of pre-proved rules for the efficient modelling, development, and analysis of networked systems. We take into account both qualitative and quantitative analysis of networks via varied formal tool support, using a theorem prover the Rodin platform and a statistical model checker the SMC-Uppaal.

Fluid dynamic modelling and simulation of circulating fluidized bed reactors: importance of the interface turbulence transfer

The main objective of this work is to analyze the importance of the gas-solid interface transfer of the kinetic energy of the turbulent motion on the accuracy of prediction of the fluid dynamic of Circulating Fluidized Bed (CFB) reactors. CFB reactors are used in a variety of industrial applications related to combustion, incineration and catalytic cracking. In this work a two-dimensional fluid dynamic model for gas-particle flow has been used to compute the porosity, the pressure, and the velocity fields of both phases in 2-D axisymmetrical cylindrical co-ordinates. The fluid dynamic model is based on the two fluid model approach in which both phases are considered to be continuous and fully interpenetrating. CFB processes are essentially turbulent. The model of effective stress on each phase is that of a Newtonian fluid, where the effective gas viscosity was calculated from the standard k-epsilon turbulence model and the transport coefficients of the particulate phase were calculated from the kinetic theory of granular flow (KTGF). This work shows that the turbulence transfer between the phases is very important for a better representation of the fluid dynamics of CFB reactors, especially for systems with internal recirculation and high gradients of particle concentration. Two systems with different characteristics were analyzed. The results were compared with experimental data available in the literature. The results were obtained by using a computer code developed by the authors. The finite volume method with collocated grid, the hybrid interpolation scheme, the false time step strategy and SIMPLEC (Semi-Implicit Method for Pressure Linked Equations - Consistent) algorithm were used to obtain the numerical solution.

Petri Net approach for modelling system integration in intelligent buildings

In this paper, a Petri Net approach is introduced for modelling and simulation of control strategies in Intelligent Building. In this context, it is claimed that integration with other building systems can be achieved in a more systematic way considering a mechatronic approach (i.e. multidisciplinary concepts applied to the development of systems). The case study is the Ambulatory Building of Medical School Hospital of University of São Paulo. Particularly, the developed methodology is applied to the elevator system and to the HVAC (Heating, Ventilation and Air Conditioning) system. It is shown that using this approach, the control systems could be integrated, improving performance.

GIS assessing traditional and modern agricultural land use/land cover change. A case study 1959-2005: Rekijoki, Somero, SW-Finland

Finland’s rural landscape has gone through remarkable changes from the 1950’s, due to agricultural developments. Changed farming practices have influenced especially traditional landscape management, and modifications in the arable land structure and grasslands transitions are notable. The review of the previous studies reveal the importance of the rural landscape composition and structure to species and landscape diversity, whereas including the relevance in presence of the open ditches, size of the field and meadow patches, topology of the natural and agricultural landscape. This land-change study includes applying remote sensed data from two time series and empirical geospatial analysis in Geographic Information Systems (GIS). The aims of this retrospective research is to detect agricultural landscape use and land cover change (LULCC) dynamics and discuss the consequences of agricultural intensification to landscape structure covering from the aspects of landscape ecology. Measurements of LULC are derived directly from pre-processed aerial images by a variety of analytical procedures, including statistical methods and image interpretation. The methodological challenges are confronted in the process of landscape classification and combining change detection approaches with landscape indices. Particular importance is paid on detecting agricultural landscape features at a small scale, demanding comprehensive understanding of such agroecosystems. Topological properties of the classified arable land and valley are determined in order to provide insight and emphasize the aspect the field edges in the agricultural landscape as important habitat. Change detection dynamics are presented with change matrix and additional calculations of gain, loss, swap, net change, change rate and tendencies are made. Transition’s possibility is computed following Markov’s probability model and presented with matrix, as well. Thesis’s spatial aspect is revealed with illustrative maps providing knowledge of location of the classified landscape categories and location of the dynamics of the changes occurred. It was assured that in Rekijoki valley’s landscape, remarkable changes in landscape has occurred. Landscape diversity has been strongly influenced by modern agricultural landscape change, as NP of open ditches has decreased and the MPS of the arable plot has decreased. Overall change in the diversity of the landscape is determined with the decrease of SHDI. Valley landscape considered as traditional land use area has experienced major transitional changes, as meadows class has lost almost one third of the area due to afforestation. Also, remarkable transitions have occurred from forest to meadow and arable land to built area. Boundaries measurement between modern and traditional landscape has indicated noticeable proportional increase in arable land-forest edge type and decrease in arable land-meadow edge type. Probability calculations predict higher future changes for traditional landscape, but also for arable land turning into built area.

Energy-efficient control strategies for variable speed driven parallel pumping systems based on pump operation point monitoring with frequency converters

The pumping processes requiring wide range of flow are often equipped with parallelconnected centrifugal pumps. In parallel pumping systems, the use of variable speed control allows that the required output for the process can be delivered with a varying number of operated pump units and selected rotational speed references. However, the optimization of the parallel-connected rotational speed controlled pump units often requires adaptive modelling of both parallel pump characteristics and the surrounding system in varying operation conditions. The available information required for the system modelling in typical parallel pumping applications such as waste water treatment and various cooling and water delivery pumping tasks can be limited, and the lack of real-time operation point monitoring often sets limits for accurate energy efficiency optimization. Hence, alternatives for easily implementable control strategies which can be adopted with minimum system data are necessary. This doctoral thesis concentrates on the methods that allow the energy efficient use of variable speed controlled parallel pumps in system scenarios in which the parallel pump units consist of a centrifugal pump, an electric motor, and a frequency converter. Firstly, the suitable operation conditions for variable speed controlled parallel pumps are studied. Secondly, methods for determining the output of each parallel pump unit using characteristic curve-based operation point estimation with frequency converter are discussed. Thirdly, the implementation of the control strategy based on real-time pump operation point estimation and sub-optimization of each parallel pump unit is studied. The findings of the thesis support the idea that the energy efficiency of the pumping can be increased without the installation of new, more efficient components in the systems by simply adopting suitable control strategies. An easily implementable and adaptive control strategy for variable speed controlled parallel pumping systems can be created by utilizing the pump operation point estimation available in modern frequency converters. Hence, additional real-time flow metering, start-up measurements, and detailed system model are unnecessary, and the pumping task can be fulfilled by determining a speed reference for each parallel-pump unit which suggests the energy efficient operation of the pumping system.

Phytosociology in agricultural areas submitted to distinct wintercropping management

Studies related to weed dynamics are essential for agricultural sustainability in tropical soils, as their interference can cause significant yield losses, especially in crops with lower competitive ability. This study aimed to assess the composition of weed communities in the third cropping season in areas submitted to distinct wintercroppings for two consecutive years. Evaluations were made in terms of species composition, level of infestation, and severity of occurrence of each weed species in relation to the others within the same area. The wintercropping management systems were: (1) Brachiaria ruziziensis; (2) corn intercropped with B. ruziziensis; (3) corn and (4) cowpea. Plant communities under these wintercrop systems were evaluated in the third year in terms of relative frequency, relative dominance, relative abundance and importance index for each species. Areas were also compared in terms of species composition by the Sorensen's similarity coefficient. Two years of distinct wintercrop managements were not enough to cause a significant shift in terms of weed composition and severity in a given area. There is also evidence that some weed species are more favored by specific crops, although the causes of this selective behavior are not fully explored in this article. The presence of B. ruziziensis, either alone or intercropped with corn, resulted in lower similarity coefficients when compared to areas where this species was not present. It is suggested that several mechanisms briefly discussed may be involved in the impact of the presence of B. ruziziensis on the weed community.

DETECTION OF GLYPHOSATE-RESISTANT PALMER AMARANTH (Amaranthus palmeri) IN AGRICULTURAL AREAS OF MATO GROSSO, BRAZIL

ABSTRACT The recent introduction of Palmer amaranth (Amaranthus palmeri) in Brazilian agricultural areas may promote several changes on weed management, especially in no-till systems and in glyphosate-resistant crops, since glyphosate-resistant biotypes of A. palmerihave been frequently selected in other countries. Therefore, this research was developed in order to evaluate the glyphosate susceptibility of a Palmer amaranth biotype recently identified in the State of Mato Grosso, Brazil. For this purpose, glyphosate susceptibility of three Amaranthusbiotypes was compared: A.hybridus var. patulus, collected in the State of Rio Grande do Sul - Brazil; A.hybridus var. patulus, collected in the State of São Paulo - Brazil; and A.palmeri, collected in the State of Mato Grosso - Brazil. Dose-response curves were generated for all biotypes, considering eight rates of glyphosate and six replicates. All the experiments were repeated twice. Both A.hybridus biotypes were satisfactorily controlled by glyphosate, demanding rates equal to or lower than 541.15 g a.e. ha-1 for 80% control (LD80). The A.palmeri biotype was not controlled by glyphosate in any of the assessments and required rates greater than 4,500 g a.e. ha-1 to reach LD80, which are economically and environmentally unacceptable. Comparison of the Brazilian A.palmeri biotype to the A. hybridus biotypes, as well as, to the results available in scientific international literature, led to the conclusion that the Brazilian Palmer amaranth biotype is resistant to glyphosate.

Weed Phytosociological and Floristic Survey in Agricultural Areas of Southwestern Goiás Region

The use of the Roundup Ready(r) technology and the cultivation of a second crop influence the floristic composition of weed communities in Brazilian Central-West region cropping systems. This study has aimed to diagnose the dominant weed species in southwestern Goiás in areas of genetically-modified and conventional soybeans, using phytosociological and floristic surveys. Weed sampling was obtained by collecting all the plants present within a 0.5 m hollow frame, randomly thrown 20 times in each of thirty-five agricultural areas in the 2012/2013 harvest. Field survey was carried out in three periods: before desiccation for soybean sowing, before postemergence herbicide in soybean first application and before postemergence herbicide application in late harvest. A total of 525 m2 was inventoried and 3,219 weeds were collected, which included 79 species, 58 genera and 28 families. Families Poaceae, Asteraceae, Euphorbiaceae, Fabaceae, Amaranthaceae, were the most representative in the survey. Species Cenchrus echinatus, Glycine max, Chamaesyce hirta, Commelina benghalensis, and Alternanthera tenella stood out in importance. The RR+millet soybean treatment had the highest number of species (44), while the conventional soybean + sorghum treatment had the lowest number of species (18). The highest number of species was recorded in first sampling period. Treatments conventional soybean + maize and conventional soybean + millet showed higher similarity (70%), while treatments RR soybean + millet and conventional soybean + sorghum showed the least (51%). Species of difficult control were recorded in all cultivation systems analyzed.

Energy and Dynamics of the solar agricultural robot "SolarSprayer"

The main objective of the present study was to design an agricultural robot, which work is based on the generation of the electricity by the solar panel. To achieve the proper operation of the robot according to the assumed working cycle the detailed design of the main equipment was made. By analysing the possible areas of implementation together with developments, the economic forecast was held. As a result a decision about possibility of such device working in agricultural sector was made and the probable topics of the further study were found out.

Analysis and modelling of chemical looping combustion process with and without oxygen uncoupling

Effective control and limiting of carbon dioxide (CO₂) emissions in energy production are major challenges of science today. Current research activities include the development of new low-cost carbon capture technologies, and among the proposed concepts, chemical combustion (CLC) and chemical looping with oxygen uncoupling (CLOU) have attracted significant attention allowing intrinsic separation of pure CO₂ from a hydrocarbon fuel combustion process with a comparatively small energy penalty. Both CLC and CLOU utilize the well-established fluidized bed technology, but several technical challenges need to be overcome in order to commercialize the processes. Therefore, development of proper modelling and simulation tools is essential for the design, optimization, and scale-up of chemical looping-based combustion systems. The main objective of this work was to analyze the technological feasibility of CLC and CLOU processes at different scales using a computational modelling approach. A onedimensional fluidized bed model frame was constructed and applied for simulations of CLC and CLOU systems consisting of interconnected fluidized bed reactors. The model is based on the conservation of mass and energy, and semi-empirical correlations are used to describe the hydrodynamics, chemical reactions, and transfer of heat in the reactors. Another objective was to evaluate the viability of chemical looping-based energy production, and a flow sheet model representing a CLC-integrated steam power plant was developed. The 1D model frame was succesfully validated based on the operation of a 150 kWth laboratory-sized CLC unit fed by methane. By following certain scale-up criteria, a conceptual design for a CLC reactor system at a pre-commercial scale of 100 MWth was created, after which the validated model was used to predict the performance of the system. As a result, further understanding of the parameters affecting the operation of a large-scale CLC process was acquired, which will be useful for the practical design work in the future. The integration of the reactor system and steam turbine cycle for power production was studied resulting in a suggested plant layout including a CLC boiler system, a simple heat recovery setup, and an integrated steam cycle with a three pressure level steam turbine. Possible operational regions of a CLOU reactor system fed by bituminous coal were determined via mass, energy, and exergy balance analysis. Finally, the 1D fluidized bed model was modified suitable for CLOU, and the performance of a hypothetical 500 MWth CLOU fuel reactor was evaluated by extensive case simulations.

Rigorous development of safety-critical systems

Nowadays, computer-based systems tend to become more complex and control increasingly critical functions affecting different areas of human activities. Failures of such systems might result in loss of human lives as well as significant damage to the environment. Therefore, their safety needs to be ensured. However, the development of safety-critical systems is not a trivial exercise. Hence, to preclude design faults and guarantee the desired behaviour, different industrial standards prescribe the use of rigorous techniques for development and verification of such systems. The more critical the system is, the more rigorous approach should be undertaken. To ensure safety of a critical computer-based system, satisfaction of the safety requirements imposed on this system should be demonstrated. This task involves a number of activities. In particular, a set of the safety requirements is usually derived by conducting various safety analysis techniques. Strong assurance that the system satisfies the safety requirements can be provided by formal methods, i.e., mathematically-based techniques. At the same time, the evidence that the system under consideration meets the imposed safety requirements might be demonstrated by constructing safety cases. However, the overall safety assurance process of critical computerbased systems remains insufficiently defined due to the following reasons. Firstly, there are semantic differences between safety requirements and formal models. Informally represented safety requirements should be translated into the underlying formal language to enable further veri cation. Secondly, the development of formal models of complex systems can be labour-intensive and time consuming. Thirdly, there are only a few well-defined methods for integration of formal verification results into safety cases. This thesis proposes an integrated approach to the rigorous development and verification of safety-critical systems that (1) facilitates elicitation of safety requirements and their incorporation into formal models, (2) simplifies formal modelling and verification by proposing specification and refinement patterns, and (3) assists in the construction of safety cases from the artefacts generated by formal reasoning. Our chosen formal framework is Event-B. It allows us to tackle the complexity of safety-critical systems as well as to structure safety requirements by applying abstraction and stepwise refinement. The Rodin platform, a tool supporting Event-B, assists in automatic model transformations and proof-based verification of the desired system properties. The proposed approach has been validated by several case studies from different application domains.

Semantic and fuzzy modelling for human behaviour recognition in smart spaces : a case study on ambient assisted living.

Human activity recognition in everyday environments is a critical, but challenging task in Ambient Intelligence applications to achieve proper Ambient Assisted Living, and key challenges still remain to be dealt with to realize robust methods. One of the major limitations of the Ambient Intelligence systems today is the lack of semantic models of those activities on the environment, so that the system can recognize the speci c activity being performed by the user(s) and act accordingly. In this context, this thesis addresses the general problem of knowledge representation in Smart Spaces. The main objective is to develop knowledge-based models, equipped with semantics to learn, infer and monitor human behaviours in Smart Spaces. Moreover, it is easy to recognize that some aspects of this problem have a high degree of uncertainty, and therefore, the developed models must be equipped with mechanisms to manage this type of information. A fuzzy ontology and a semantic hybrid system are presented to allow modelling and recognition of a set of complex real-life scenarios where vagueness and uncertainty are inherent to the human nature of the users that perform it. The handling of uncertain, incomplete and vague data (i.e., missing sensor readings and activity execution variations, since human behaviour is non-deterministic) is approached for the rst time through a fuzzy ontology validated on real-time settings within a hybrid data-driven and knowledgebased architecture. The semantics of activities, sub-activities and real-time object interaction are taken into consideration. The proposed framework consists of two main modules: the low-level sub-activity recognizer and the high-level activity recognizer. The rst module detects sub-activities (i.e., actions or basic activities) that take input data directly from a depth sensor (Kinect). The main contribution of this thesis tackles the second component of the hybrid system, which lays on top of the previous one, in a superior level of abstraction, and acquires the input data from the rst module's output, and executes ontological inference to provide users, activities and their in uence in the environment, with semantics. This component is thus knowledge-based, and a fuzzy ontology was designed to model the high-level activities. Since activity recognition requires context-awareness and the ability to discriminate among activities in di erent environments, the semantic framework allows for modelling common-sense knowledge in the form of a rule-based system that supports expressions close to natural language in the form of fuzzy linguistic labels. The framework advantages have been evaluated with a challenging and new public dataset, CAD-120, achieving an accuracy of 90.1% and 91.1% respectively for low and high-level activities. This entails an improvement over both, entirely data-driven approaches, and merely ontology-based approaches. As an added value, for the system to be su ciently simple and exible to be managed by non-expert users, and thus, facilitate the transfer of research to industry, a development framework composed by a programming toolbox, a hybrid crisp and fuzzy architecture, and graphical models to represent and con gure human behaviour in Smart Spaces, were developed in order to provide the framework with more usability in the nal application. As a result, human behaviour recognition can help assisting people with special needs such as in healthcare, independent elderly living, in remote rehabilitation monitoring, industrial process guideline control, and many other cases. This thesis shows use cases in these areas.

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.

Computational models for and from biology : simple gene assembly and reaction systems

The advancement of science and technology makes it clear that no single perspective is any longer sufficient to describe the true nature of any phenomenon. That is why the interdisciplinary research is gaining more attention overtime. An excellent example of this type of research is natural computing which stands on the borderline between biology and computer science. The contribution of research done in natural computing is twofold: on one hand, it sheds light into how nature works and how it processes information and, on the other hand, it provides some guidelines on how to design bio-inspired technologies. The first direction in this thesis focuses on a nature-inspired process called gene assembly in ciliates. The second one studies reaction systems, as a modeling framework with its rationale built upon the biochemical interactions happening within a cell. The process of gene assembly in ciliates has attracted a lot of attention as a research topic in the past 15 years. Two main modelling frameworks have been initially proposed in the end of 1990s to capture ciliates’ gene assembly process, namely the intermolecular model and the intramolecular model. They were followed by other model proposals such as templatebased assembly and DNA rearrangement pathways recombination models. In this thesis we are interested in a variation of the intramolecular model called simple gene assembly model, which focuses on the simplest possible folds in the assembly process. We propose a new framework called directed overlap-inclusion (DOI) graphs to overcome the limitations that previously introduced models faced in capturing all the combinatorial details of the simple gene assembly process. We investigate a number of combinatorial properties of these graphs, including a necessary property in terms of forbidden induced subgraphs. We also introduce DOI graph-based rewriting rules that capture all the operations of the simple gene assembly model and prove that they are equivalent to the string-based formalization of the model. Reaction systems (RS) is another nature-inspired modeling framework that is studied in this thesis. Reaction systems’ rationale is based upon two main regulation mechanisms, facilitation and inhibition, which control the interactions between biochemical reactions. Reaction systems is a complementary modeling framework to traditional quantitative frameworks, focusing on explicit cause-effect relationships between reactions. The explicit formulation of facilitation and inhibition mechanisms behind reactions, as well as the focus on interactions between reactions (rather than dynamics of concentrations) makes their applicability potentially wide and useful beyond biological case studies. In this thesis, we construct a reaction system model corresponding to the heat shock response mechanism based on a novel concept of dominance graph that captures the competition on resources in the ODE model. We also introduce for RS various concepts inspired by biology, e.g., mass conservation, steady state, periodicity, etc., to do model checking of the reaction systems based models. We prove that the complexity of the decision problems related to these properties varies from P to NP- and coNP-complete to PSPACE-complete. We further focus on the mass conservation relation in an RS and introduce the conservation dependency graph to capture the relation between the species and also propose an algorithm to list the conserved sets of a given reaction system.