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.

The requirements of a feasible plastic packaging material for cultured dairy products

The objective of this Master´s Thesis was to conduct a wide scale preliminary survey regarding the package requirements of a cultured dairy package, and to compare the currently used material polystyrene to other suitable packaging materials. Polystyrene has a long history of use in dairy cups, but in recent years its price has increased significantly compared to other common packaging materials. The overall environmental effects of a package and a package material are today a part of designing a sustainable product life cycle. In addition, in certain contexts there has been discussion of the risks posed by styrene polymer for the environment and for humans. These risks are also discussed in this thesis. Polystyrene (PS) is still the most widely used material in dairy cups. In recent years, polypropylene (PP) cups have appeared in increasing numbers on market shelves. This study focuses on the differences of the suitable polymers and examines the suitability of alternative “suitable” polymers with regards to dairy packaging. Aside from focusing on the cup manufacturer, this thesis also examines its subject matter from the viewpoint of the dairy customer, as well as observing the concrete implications of material changes in the overall value chain. It was known in advance that material permeability would be one of the determining factors and that gas transmission testing would be a significant part of the thesis. Mechanical tests were the second part of the testing process, providing information regarding package strength and protectiveness during the package’s life cycle. Production efficiency, along with uninterrupted stable production, was another important factor that was taken into consideration. These two issues are sometimes neglected in similar contexts due to their self-evident nature. In addition, materials used in production may have a surprising significance to the production and efficiency. Consistent high quality is also partly based on material selection. All of the aforementioned factors have been documented and the results have been analyzed by the development team at Coveris Rigid Finland. Coveris is now calculating the total finance effects and capacities should the material changes be implemented in practice. There are many factors in favor of switching to polypropylene at the moment. The overall production costs, as well as the environmental effects of resin production are the primary influences for said switch from the converters’ perspective.

The requirements and needs of global data usage in product lifecycle management

This study was done for ABB Ltd. Motors and Generators business unit in Helsinki. In this study, global data movement in large businesses is examined from a product data management (PDM) and enterprise resource planning (ERP) point-of-view. The purpose of this study was to understand and map out how a large global business handles its data in a multiple site structure and how it can be applied in practice. This was done by doing an empirical interview study on five different global businesses with design locations in multiple countries. Their master data management (MDM) solutions were inspected and analyzed to understand which solution would best benefit a large global architecture with many design locations. One working solution is a transactional hub which negates the effects of multisite transfers and reduces lead times. Also, the requirements and limitations of the current MDM architecture were analyzed and possible reform ideas given.  

A multimethod examination of contributors to successful on-the-job learning for vocational students

Rapid changes in working life and competence requirements of different professions have increased interest in workplace learning. It is considered an effective way to learn and update professional skills by performing daily tasks in an authentic environment. Especially, ensuring a supply of skilled future workers is a crucial issue for firms facing tight competition and a shortage of competent employees due to the retirement of current professionals. In order to develop and make the most of workplace learning, it is important to focus on workplace learning environments and the individual characteristics of those participating in workplace learning. The literature has suggested various factors that influence adults' and professionals’ workplace learning of profession-related skills, but lacks empirical studies on contextual and individual-related factors that positively affect students' workplace learning. Workers with vocational education form a large group in modern firms. Therefore, elements of vocational students’ successful workplace learning during their studies, before starting their career paths, need to be examined. To fill this gap in the literature, this dissertation examines contributors to vocational students’ workplace learning in Finland, where students’ workplace learning is included in the vocational education and training system. The study is divided into two parts: the introduction, comprised of the overview of the relevant literature and the conclusion of the entire study, and five separate articles. Three of the articles utilize quantitative methods and two use qualitative methods to examine factors that contribute to vocational students’ workplace learning. The results show that, from the students’ perspective, attitudinal, motivational, and organizationrelated factors enhance the student’s development of professionalism during the on-the-job learning period. Specifically, the organization-related factors such as innovative climate, guidance, and interactions with seniors have a strong positive impact on the students’ perceived development of professional skills because, for example, the seniors’ guidance and provision of new viewpoints for the tasks helps the vocational students to gain autonomy at work performance. A multilevel analysis shows that of those factors enhancing workplace learning from the student perspective, innovative climate, knowledge transfer accuracy, and the students’ performance orientation were significantly related to the workplace instructors’ assessment regarding the students’ professional performance. Furthermore, support from senior colleagues and the students’ self-efficacy were both significantly associated with the formal grades measuring how well the students managed to learn necessary professional skills. In addition, the results suggest that the students’ on-the-job learning can be divided into three main phases, of which two require efforts from both the student and the on-the-job learning organization. The first phase includes the student’s application of basic professional skills, demonstration of potential in performing daily tasks, and orientation provided by the organization at the beginning of the on-the-job learning period. In the second phase, the student actively develops profession-related skills by performing daily tasks, thus learning a fluent working style while observing the seniors’ performance. The organization offers relevant tasks and follows the student’s development. The third level indicates a student who has reached the professional level described as a full occupation. The results suggest that constructing the vocational students’ successful on-the-job learning period requires feedback from seniors, opportunities to learn to manage entire work processes, self-efficacy on the part of the students, proactive behavior, and initiative in learning. The study contributes to research on workplace learning in three ways: firstly, it identifies the key individual- and organization-based factors that influence the vocational students’ successful on-the-job learning from their perspective and examines mutual relationships between these factors. Second, the study provides knowledge of how the factors related to the students’ view of successful workplace learning are associated with the workplace instructors’ perspective and the formal grades. Third, the present study finds elements needed to construct a successful on-the-job learning for the students.

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.

Protein turnover, amino acid requirements and recommendations for athletes and active populations

Skeletal muscle is the major deposit of protein molecules. As for any cell or tissue, total muscle protein reflects a dynamic turnover between net protein synthesis and degradation. Noninvasive and invasive techniques have been applied to determine amino acid catabolism and muscle protein building at rest, during exercise and during the recovery period after a single experiment or training sessions. Stable isotopic tracers (13C-lysine, 15N-glycine, ²H5-phenylalanine) and arteriovenous differences have been used in studies of skeletal muscle and collagen tissues under resting and exercise conditions. There are different fractional synthesis rates in skeletal muscle and tendon tissues, but there is no major difference between collagen and myofibrillar protein synthesis. Strenuous exercise provokes increased proteolysis and decreased protein synthesis, the opposite occurring during the recovery period. Individuals who exercise respond differently when resistance and endurance types of contractions are compared. Endurance exercise induces a greater oxidative capacity (enzymes) compared to resistance exercise, which induces fiber hypertrophy (myofibrils). Nitrogen balance (difference between protein intake and protein degradation) for athletes is usually balanced when the intake of protein reaches 1.2 g·kg-1·day-1 compared to 0.8 g·kg-1·day-1 in resting individuals. Muscular activities promote a cascade of signals leading to the stimulation of eukaryotic initiation of myofibrillar protein synthesis. As suggested in several publications, a bolus of 15-20 g protein (from skimmed milk or whey proteins) and carbohydrate (± 30 g maltodextrine) drinks is needed immediately after stopping exercise to stimulate muscle protein and tendon collagen turnover within 1 h.

Pró-vitaminas A em hortaliças comercializadas no mercado formal e informal de Viçosa (MG), em três estações do ano

Para fornecer dados sobre a influência climática e a forma de comercialização sobre carotenóides de vegetais, este estudo pesquisou o conteúdo de alfa e beta-caroteno e o valor de vitamina A de sete hortaliças (batata-doce, cenoura, moranga, pimentão, quiabo, tomate e vagem), na cidade de Viçosa (MG), utilizando a Cromatografia Líquida de Alta Eficiência. Compararam-se hortaliças comercializadas nos mercados formal (mercados locais) e informal (feira livre) durante primavera, verão e outono. A cenoura apresentou os teores mais elevados de alfa e beta-caroteno (31,17 e 58,18 µg/g, respectivamente), seguida pela moranga (4,33 e 23,16 µg/g, respectivamente), enquanto a batata-doce apresentou o teor mais reduzido de beta-caroteno (0,51 µg/g). O valor de vitamina A variou conforme o perfil de alfa e beta-caroteno. Com exceção da cenoura e do quiabo, não houve influência significativa do local de comercialização sobre o conteúdo de carotenóides. A variação do conteúdo de carotenos nas estações do ano foi inexpressiva, sendo que apenas o pimentão apresentou valores significativamente diferentes. Porções de 100 g das hortaliças analisadas fornecem entre 3 e 78% da recomendação de vitamina A.

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.

Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.

Determinantes da recuperação do emprego formal no Brasil: evidências para o período 2001/2005 e hipoteses para uma agenda de pesquisa

Decisive factors affecting the recent increase in formal employment in Brazil. This paper gives a general overview of the evolution of labour market indicators between 1995 and 2005 in Brazil. It shows an overall increase in formal employment rates from 2001 to 2005, as opposite to what had happened from 1995 to 1999. It is argued that such recent trends might indicate the reconfiguration of the labour market in better terms, with potential positive consequences to the finance performance of the Social Security sector. The paper also examines some of the major factors associated with this new trend and their chances to maintain such tendency in the near future. It's important to notice that all of them may be subject to some kind of political management by the State. In other words, we suggest that there are suficient instruments and operative skills in the Brazilian State to make these and others factors work in favour of a more persistent strategy of development with social inclusion through labour.