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.

Identification of characteristics for successful university-company partnership development

The importance of university-company collaboration has increased during the last decades. The drivers for that are, on the one hand, changes in business logic of companies and on the other hand the decreased state funding of universities. Many companies emphasize joint research with universities as an enabling input to their development processes, which aim at creating new innovations, products and wealth. These factors have changed universities’ operations and they have adopted several practices of dynamic business organizations, such as strategic planning, monitoring and controlling methods of internal processes etc. The objective of this thesis is to combine different characteristics of successful university-company partnership and its development. The development process starts with identifying potential partners in the university’s interest group, which requires understanding the role of different partners in the innovation system. Next, in order to find a common development basis, matching the policy and strategy between partners is needed. The third phase is to combine the academic and industrial objectives of a joint project, which is a typical form of university-company collaboration. The optimum is a win-win situation where both partners, universities and companies, can get addedvalue. For the companies added value typically means access to new research results before their competitors. For the universities added value offers a possibility to carry on high level scientific work. The research output in the form of published scientific articles is evaluated by the international science community. Because the university-company partnership is often executed by joint projects, the different forms of this kind of projects is discussed in this study. The most challenging form of collaboration is a semi-open project model, which is not based on bilateral activities between universities and companies but on a consortium of several universities, research institutes and companies. The universities and companies are core actors in the innovation system. Thus the discussion of their roles and relations to public operators like publicly funded financiers is important. In the Finnish innovation system there are at least the following doers executing strategies and policies: EU, Academy of Finland and TEKES. In addition to these, Strategic Centres for Science, Technology and Innovation which are owned jointly by companies, universities and research organizations have a very important role in their fields of business. They transfer research results into commercial actions to generate wealth. The thesis comprises two parts. The first part consists of an overview of the study including introduction, literature review, research design, synthesis of findings and conclusions. The second part introduces four original research publications.

Feasibility of industrial implementation of laser cutting into paper making machine

Laser cutting implementation possibilities into paper making machine was studied as the main objective of the work. Laser cutting technology application was considered as a replacement tool for conventional cutting methods used in paper making machines for longitudinal cutting such as edge trimming at different paper making process and tambour roll slitting. Laser cutting of paper was tested in 70’s for the first time. Since then, laser cutting and processing has been applied for paper materials with different level of success in industry. Laser cutting can be employed for longitudinal cutting of paper web in machine direction. The most common conventional cutting methods include water jet cutting and rotating slitting blades applied in paper making machines. Cutting with CO2 laser fulfils basic requirements for cutting quality, applicability to material and cutting speeds in all locations where longitudinal cutting is needed. Literature review provided description of advantages, disadvantages and challenges of laser technology when it was applied for cutting of paper material with particular attention to cutting of moving paper web. Based on studied laser cutting capabilities and problem definition of conventional cutting technologies, preliminary selection of the most promising application area was carried out. Laser cutting (trimming) of paper web edges in wet end was estimated to be the most promising area where it can be implemented. This assumption was made on the basis of rate of web breaks occurrence. It was found that up to 64 % of total number of web breaks occurred in wet end, particularly in location of so called open draws where paper web was transferred unsupported by wire or felt. Distribution of web breaks in machine cross direction revealed that defects of paper web edge was the main reason of tearing initiation and consequent web break. The assumption was made that laser cutting was capable of improvement of laser cut edge tensile strength due to high cutting quality and sealing effect of the edge after laser cutting. Studies of laser ablation of cellulose supported this claim. Linear energy needed for cutting was calculated with regard to paper web properties in intended laser cutting location. Calculated linear cutting energy was verified with series of laser cutting. Practically obtained laser energy needed for cutting deviated from calculated values. This could be explained by difference in heat transfer via radiation in laser cutting and different absorption characteristics of dry and moist paper material. Laser cut samples (both dry and moist (dry matter content about 25-40%)) were tested for strength properties. It was shown that tensile strength and strain break of laser cut samples are similar to corresponding values of non-laser cut samples. Chosen method, however, did not address tensile strength of laser cut edge in particular. Thus, the assumption of improving strength properties with laser cutting was not fully proved. Laser cutting effect on possible pollution of mill broke (recycling of trimmed edge) was carried out. Laser cut samples (both dry and moist) were tested on the content of dirt particles. The tests revealed that accumulation of dust particles on the surface of moist samples can take place. This has to be taken into account to prevent contamination of pulp suspension when trim waste is recycled. Material loss due to evaporation during laser cutting and amount of solid residues after cutting were evaluated. Edge trimming with laser would result in 0.25 kg/h of solid residues and 2.5 kg/h of lost material due to evaporation. Schemes of laser cutting implementation and needed laser equipment were discussed. Generally, laser cutting system would require two laser sources (one laser source for each cutting zone), set of beam transfer and focusing optics and cutting heads. In order to increase reliability of system, it was suggested that each laser source would have double capacity. That would allow to perform cutting employing one laser source working at full capacity for both cutting zones. Laser technology is in required level at the moment and do not require additional development. Moreover, capacity of speed increase is high due to availability high power laser sources what can support the tendency of speed increase of paper making machines. Laser cutting system would require special roll to maintain cutting. The scheme of such roll was proposed as well as roll integration into paper making machine. Laser cutting can be done in location of central roll in press section, before so-called open draw where many web breaks occur, where it has potential to improve runability of a paper making machine. Economic performance of laser cutting was done as comparison of laser cutting system and water jet cutting working in the same conditions. It was revealed that laser cutting would still be about two times more expensive compared to water jet cutting. This is mainly due to high investment cost of laser equipment and poor energy efficiency of CO2 lasers. Another factor is that laser cutting causes material loss due to evaporation whereas water jet cutting almost does not cause material loss. Despite difficulties of laser cutting implementation in paper making machine, its implementation can be beneficial. The crucial role in that is possibility to improve cut edge strength properties and consequently reduce number of web breaks. Capacity of laser cutting to maintain cutting speeds which exceed current speeds of paper making machines what is another argument to consider laser cutting technology in design of new high speed paper making machines.

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.

The role of business model in computer game development organizations

The computer game industry has grown steadily for years, and in revenues it can be compared to the music and film industries. The game industry has been moving to digital distribution. Computer gaming and the concept of business model are discussed among industrial practitioners and the scientific community. The significance of the business model concept has increased in the scientific literature recently, although there is still a lot of discussion going on on the concept. In the thesis, the role of the business model in the computer game industry is studied. Computer game developers, designers, project managers and organization leaders in 11 computer game companies were interviewed. The data was analyzed to identify the important elements of computer game business model, how the business model concept is perceived and how the growth of the organization affects the business model. It was identified that the importance of human capital is crucial to the business. As games are partly a product of creative thinking also innovation and the creative process are highly valued. The same applies to technical skills when performing various activities. Marketing and customer relationships are also considered as key elements in the computer game business model. Financing and partners are important especially for startups, when the organization is dependent on external funding and third party assets. The results of this study provide organizations with improved understanding on how the organization is built and what business model elements are weighted.

Development of modular roll service concepts

The goal of this study was to find and develop new or improved service concepts for rolls in a paper machine and secondary targets were to find out what the KPIs and values of the concepts are. Two methodologies were utilized in researching this problem; firstly sales personnel were interviewed about customer values and KPIs and a questionnaire about service modules were sent out to four BSI (basic sales item) responsible persons. Throughout the research process differences in geographic regions were identified and several customer KPIs and values were discovered. The interviews showed that the main concern for customers is the cost of operations. The goal is to produce the same or in some cases more tons with smaller operating costs. The questionnaire standardized the data about service modules and made it possible to link these values, KPIs and concerns of customers to Valmet’s service offering. Eventually these service modules were used to create a service concepts that offer flexibility, cost savings, safety and peace of mind for the customers. With this new conceptual approach Valmet can more flexibly answer to customer quotations and modify the offering to better generate customer value and customer satisfaction. In addition a new BSI was defined and proposed for pilot projects.

Política industrial e desenvolvimento

This paper aims at contributing to the debate on industrial policy and economic development in Brazil. At first, theoretical approaches that support industrial policy-making are discussed, with emphasis on the neoschumpeterian/evolutionary approach, which focuses on innovation as prime mover of economic development and on the co-evolution of technologies, institutions, and industries and firms structures. Next, such an approach is applied to explain some successful experiences of industrial policy-making and economic development in Brazil up to the end of the 1970s, and the failures to implement such a policy from the 1980s onwards. Finally, the present government industrial policy is evaluated, arguing that although it has some positive aspects like the focus on innovation, clearly defined targets and a new institutional organization, it fails as an economic development policy because of weaknesses such as incompatibility with macroeconomic policy, inconsistencies of policy instruments, deficiencies in infrastructure and in the science, technology and innovation system, and lack of coordination and political drive.

The industrial equilibrium exchange rate in Brazil: an estimation

This paper presents a methodology for calculating the industrial equilibrium exchange rate, which is defined as the one enabling exporters of state-of-the-art manufactured goods to be competitive abroad. The first section highlights the causes and problems of overvalued exchange rates, particularly the Dutch disease issue, which is neutralized when the exchange rate strikes the industrial equilibrium level. This level is defined by the ratio between the unit labor cost in the country under consideration and in competing countries. Finally, the evolution of this exchange rate in the Brazilian economy is estimated.

Política industrial e desenvolvimento econômico: a reatualização de um debate histórico

Industrial policy and economic development: a review of the contemporary debate. This paper discusses the importance of the industrial policy for the Brazilian economic development. It presents the theoretical foundations and the main international experiences about this theme. Besides it examines the main industrial policies adopted in Brazil, especially in recent years. Based on this discussion, it is possible to note that despite the criticisms against this policy, they were widely used by many developed countries in the past and also played an important role, contributing to increase the industrial growth in Brazil. However, the recent Brazilian industrial policies were not so efficient, especially when compared with those adopted during most of the 20th century.

A política industrial chinesa como determinante de sua estratégia going global

China has experienced not only high rates of economic growth as well as an unprecedented competitive international insertion since the turn of the century. This process was not guided solely by market forces or influenced by Government intervention in the economy. Although much has been argued that China's "going global" strategy is rooted in state action, and especially its policy of exchange rate depreciation and trade policy incentives for exports and investments abroad, we argue that the major determinant of this strategy, which established the basic conditions for industrial competitiveness, was its industrial policy. The focus of this article is on the changes in China's industrial structure, emphasizing that Chinese industrial policy is a central determinant of its international insertion strategy.

Políticas productivas y competitividad industrial: El caso de Argentina y Brasil

This article aims, on the one hand, to analyze the increase of productive asymmetries between Argentina and Brazil that have been evidencing during the last two decades, and are currently reveled in the structural trade deficit of industrial products that affects Argentina in the bilateral relationship. On the other hand, it intends to contribute to understanding the roots of these asymmetries based on the differences in the public policies implemented by both countries during the period extending from the implementation of the Mercosur, in the early 1990s, until 2008. The focus is set on the technological pattern of industrial production and trade structures, considering a non neutral impact over the long term development.

Effects of overvaluation and exchange rate volatility over industrial investment: empirical evidence and economic policy proposals for Brazil

The present article aims to analyze the recent behavior of real exchange rate in Brazil and its effects over investment per worker in Brazilian manufacturing and extractive industry. Preliminary estimates presented in the article shows an over-valuation of 48% of real exchange rate in Brazil. The reaction between the level (and volatility) of real exchange rate and investment (per worker) in Brazil is analyzed by means of a panel data econometric model for 30 sectors of Brazilian manufacturing and extractive industry. The empirical results show that the level and volatility of real exchange rate has a strong effect over investment per worker in Brazilian industry. Finally, we conclude the article presenting a proposal for a new macroeconomic regime that aims to produce an acceleration of economic growth of Brazilian economy and, by that, a catching-up process with developed countries.

Possibilities and challenges in utilization of information provided by Industrial Internet applications

Global digitalization has affected also industrial sector. A trend called Industrial Internet has been present for some years and established relatively steady position in businesses. Industrial Internet is also referred with the terminology Industry 4.0 and in consumer businesses IoT (Internet of Things). Eventually, trend consists of many traditionally proven technologies and concepts, such as condition monitoring, remote services, predictive maintenance and Internet customer portals. All these technologies and information related to them are estimated to change the rules of business in industrial sector. This may result even a new industrial revolution. This research has its focus on Industrial Internet products, services and applications. The study analyses four case companies and their digital service offerings. According to this analysis the comparison of these services is done to find out if there is still space for companies to gain competitive advantage through differentiation with these state of the art solutions. One of the case companies, Case Company Ltd., is working as a primary case company and a subscriber of this particular research. The research and results are analyzed primarily from this company’s perspective and need. In empirical part, the research clarifies how Case Company Ltd. has allocated its development resources through last five years. These allocations in certain categories are then compared to other case companies’ current customer offering and conclusions are made how the approach of different companies differ from each other. Existing theoretical knowledge of Industrial Internet is about to find its shape. In this research we take a look how the case company analysis and findings correlate with the existing knowledge and literature of the topic.

From Fordism to neoconservatism : free trade and Canadian industrial policy in an era of globalism /

Nothing today affects the lives of people in countries throughout the industrialized and developing world as much as international trade. Nowhere is this more true than in Canada. Canada's involvement in international trade has a long history dating back to 1854 when it was a British colony. As a major trading country, Canada has always adopted a proactive industrial policy which has been largely responsible for its relative economic prosperi ty. But, wi th businesses now free to invest and divest under the terms of the CUFTA and the NAFTA, the most fundamental concerns for Canadians, in a borderless world, are what powers will the Canadian government have to shape industrial policy, and to what extent can Canada continue as a viable nationstate if it can no longer control its national economy? These are important concerns because, in world without borders, the adjustment process becomes more volatile and more difficult to manage. The CUFTA and the NAFTA not only create the rules for conducting trade, but they also establish a set of new rules for the Canadian government that will diminish its power. As a member of a new North American trading bloc, Canada will find itself subject to a set of forces requiring analysis beyond participation in a conventional free trade area. Because many of the traditional levers of government will now be subject to external control imposed by these agreements, Canada will not be able to mount certain policies in the future that it has relied on in the past. This reality limits the pro-active role of the Canadian state to use policies and programmes for the country's immediate national development. What this thesis attempts is an examination of the evolution of Canadian industrial policy, in effect, the transi tion from Fordism to Neoconservatism, and an assessment of Canada's future as a nation-state as it tries to find security and improved access in a free trade arrangement. Unless Canada takes steps to neutralize the asymmetry of power between itself and the United States through adjustment programmes, it is the contention of this thesis that its economic future is anything but stable.

Recreational Development and the Lake Erie Shore Photographs,1967

John N. Jackson was born and raised in London England. He served in the Royal Navy, acquired a B.A. and a Ph.D, conducted research for a city planning office and lectured at the University of Manchester. He joined Brock University’s faculty in 1965 as a Professor of Applied Geography. Since his retirement in 1991 he has been Professor Emeritus to Brock. Throughout his time in academia Jackson has focused his research on the history of the modern city, both throughout Europe and Canada. Jackson has also completed specific research on the Niagara Peninsula; including industrial geography, recreation along the Lake Erie shore, St. Catharines early history, the Welland Canals, railway development, comparisons across the Niagara River. While living in the Niagara region Jackson has become involved in many community events. He has been the Director for the Bruce Trail Association, President of the Welland Canals Foundation, and been involved in local historical groups throughout the Niagara region.