Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Russian market entry decision for an e-business company, the case Ampparit Inc.

The aim of the study was to examine foreign operation methods and suggest the entry mode for the Russian E-business market. Ampparit Inc. was chosen as a case company, as it operates in the e-commerce B2B type of the business by providing Witpik - media monitoring service. The concept of foreign operation method was clarified with a specific focus on Russian market peculiarities and E-business. The main focuses of the present work were to figure out the most applicable entry mode for the Russian market in case of e-business company and factors affecting the decision about entry, including risks, barriers and other aspects.

Improving Transportation and Warehousing Efficiency with Simulation-Based Decision Support Systems

Transportation and warehousing are large and growing sectors in the society, and their efficiency is of high importance. Transportation also has a large share of global carbondioxide emissions, which are one the leading causes of anthropogenic climate warming. Various countries have agreed to decrease their carbon emissions according to the Kyoto protocol. Transportation is the only sector where emissions have steadily increased since the 1990s, which highlights the importance of transportation efficiency. The efficiency of transportation and warehousing can be improved with the help of simulations, but models alone are not sufficient. This research concentrates on the use of simulations in decision support systems. Three main simulation approaches are used in logistics: discrete-event simulation, systems dynamics, and agent-based modeling. However, individual simulation approaches have weaknesses of their own. Hybridization (combining two or more approaches) can improve the quality of the models, as it allows using a different method to overcome the weakness of one method. It is important to choose the correct approach (or a combination of approaches) when modeling transportation and warehousing issues. If an inappropriate method is chosen (this can occur if the modeler is proficient in only one approach or the model specification is not conducted thoroughly), the simulation model will have an inaccurate structure, which in turn will lead to misleading results. This issue can further escalate, as the decision-maker may assume that the presented simulation model gives the most useful results available, even though the whole model can be based on a poorly chosen structure. In this research it is argued that simulation- based decision support systems need to take various issues into account to make a functioning decision support system. The actual simulation model can be constructed using any (or multiple) approach, it can be combined with different optimization modules, and there needs to be a proper interface between the model and the user. These issues are presented in a framework, which simulation modelers can use when creating decision support systems. In order for decision-makers to fully benefit from the simulations, the user interface needs to clearly separate the model and the user, but at the same time, the user needs to be able to run the appropriate runs in order to analyze the problems correctly. This study recommends that simulation modelers should start to transfer their tacit knowledge to explicit knowledge. This would greatly benefit the whole simulation community and improve the quality of simulation-based decision support systems as well. More studies should also be conducted by using hybrid models and integrating simulations with Graphical Information Systems.

Improving strategic decision-making with simulation based decision support systems

Combating climate change is one of the key tasks of humanity in the 21st century. One of the leading causes is carbon dioxide emissions due to usage of fossil fuels. Renewable energy sources should be used instead of relying on oil, gas, and coal. In Finland a significant amount of energy is produced using wood. The usage of wood chips is expected to increase in the future significantly, over 60 %. The aim of this research is to improve understanding over the costs of wood chip supply chains. This is conducted by utilizing simulation as the main research method. The simulation model utilizes both agent-based modelling and discrete event simulation to imitate the wood chip supply chain. This thesis concentrates on the usage of simulation based decision support systems in strategic decision-making. The simulation model is part of a decision support system, which connects the simulation model to databases but also provides a graphical user interface for the decisionmaker. The main analysis conducted with the decision support system concentrates on comparing a traditional supply chain to a supply chain utilizing specialized containers. According to the analysis, the container supply chain is able to have smaller costs than the traditional supply chain. Also, a container supply chain can be more easily scaled up due to faster emptying operations. Initially the container operations would only supply part of the fuel needs of a power plant and it would complement the current supply chain. The model can be expanded to include intermodal supply chains as due to increased demand in the future there is not enough wood chips located close to current and future power plants.

Public and Private Sector Decision Makers Within the Rail Baltica Growth Corridor

Transport volumes have increased and will continue to increase in European Union. Even though the growth has not been equal between different transport modes. Most of the growth has been faced on road transport. European Union aims to balance the unbalanced market shares between the modes by gaining and supporting the competitiveness of railway and waterway transport. In EU railway transportation is seen as solution to increase safety in traffic and decrease the environmental impacts of transportation. The aim of this research is to figure out how it is possible to decrease the environmental impacts by the technology already in use. Main focus of this research is in intermodality and combining the road and railway transportation. This study aims also to figure out demands and expectations towards new Rail Baltica railway route connecting Tallinn and Berlin. The research is conducted by performing a literature review about decreasing environmental impacts and combining road and rail transport. Another viewpoint is taken from the possible effects of tourism to the passenger transport on rails. Knowledge gained by literature review is deepened by additional internet questionnaire study and expert interview study. In decreasing the environmental impacts of transportation electric trains are definitely the best option providing that the electricity is generated from renewable or carbon dioxide free sources. Decrease of environmental impacts has been reached also with acceptance of larger road transport vehicles. According to interviewed passenger transport experts, the whole route from Tallinn to Berlin may not be convenient to be used in passenger transport, just because the route is too long.. In EU freight is transported mainly with semi-trailer combinations, and that is why it could be logical if huckepack trains would be used on Rail Baltica. Huckepack train allows semi-trailers to be transported on rails with time efficient loading-unloading process. Overall, Rail Baltica project is experienced as a future-oriented one and new railway alignment is seen as great alternative option for transport modes using fossil fuels.

Effect of emotions on consumer decision-making in a high involvement product adoption context

This thesis was written in order participate in the emergent discussion on the role of emotions in consumer decision-making. The goal of the thesis was to find out which emotions affect consumer decision-making, how these emotions relate to traditional process models of consumer decision-making, and how emotions and other factors affect consumer decision-making. The thesis is placed into a context of high involvement product adoption. The empirical research was conducted according to a qualitative methodology, which combined video diaries and face-to-face or Skype interviews as data collection methods. The case product category was dancing poles, and four women participated in the study. The central results indicate that emotion and cognition walk hand in hand in consumer decision-making, that consumers experience a variety of emotions during a decision-making process, and that emotions have an important effect on consumer decision-making and consumer behavior.

Managerial decision-making style : India, Bangladesh, and Finland : cultural side of the game

Julkaisumaa Intia 356 IN IND

Immediate Decision-Making and Information Needs in Intensive Care Coordination

The aim of this study was to develop a theoretical model for information integration to support the deci¬sion making of intensive care charge nurses, and physicians in charge – that is, ICU shift leaders. The study focused on the ad hoc decision-making and immediate information needs of shift leaders during the management of an intensive care unit’s (ICU) daily activities. The term ‘ad hoc decision-making’ was defined as critical judgements that are needed for a specific purpose at a precise moment with the goal of ensuring instant and adequate patient care and a fluent flow of ICU activities. Data collection and research analysis methods were tested in the identification of ICU shift leaders’ ad hoc decision-making. Decision-making of ICU charge nurses (n = 12) and physicians in charge (n = 8) was observed using a think-aloud technique in two university-affiliated Finnish ICUs for adults. The ad hoc decisions of ICU shift leaders were identified using an application of protocol analysis. In the next phase, a structured online question¬naire was developed to evaluate the immediate information needs of ICU shift leaders. A national survey was conducted in all Finnish, university-affiliated hospital ICUs for adults (n = 17). The questionnaire was sent to all charge nurses (n = 515) and physicians in charge (n = 223). Altogether, 257 charge nurses (50%) and 96 physicians in charge (43%) responded to the survey. The survey was also tested internationally in 16 Greek ICUs. From Greece, 50 charge nurses out of 240 (21%) responded to the survey. A think-aloud technique and protocol analysis were found to be applicable for the identification of the ad hoc decision-making of ICU shift leaders. During one day shift leaders made over 200 ad hoc decisions. Ad hoc decisions were made horizontally, related to the whole intensive care process, and vertically, concerning single intensive care incidents. Most of the ICU shift leaders’ ad hoc decisions were related to human resources and know-how, patient information and vital signs, and special treatments. Commonly, this ad hoc decision-making involved several multiprofessional decisions that constituted a bundle of immediate decisions and various information needs. Some of these immediate information needs were shared between the charge nurses and the physicians in charge. The majority of which concerned patient admission, the organisation and management of work, and staff allocation. In general, the information needs of charge nurses were more varied than those of physicians. It was found that many ad hoc deci-sions made by the physicians in charge produced several information needs for ICU charge nurses. This meant that before the task at hand was completed, various kinds of information was sought by the charge nurses to support the decision-making process. Most of the immediate information needs of charge nurses were related to the organisation and management of work and human resources, whereas the information needs of the physicians in charge mainly concerned direct patient care. Thus, information needs differ between professionals even if the goal of decision-making is the same. The results of the international survey confirmed these study results for charge nurses. Both in Finland and in Greece the information needs of charge nurses focused on the organisation and management of work and human resources. Many of the most crucial information needs of Finnish and Greek ICU charge nurses were common. In conclusion, it was found that ICU shift leaders make hundreds of ad hoc decisions during the course of a day related to the allocation of resources and organisation of patient care. The ad hoc decision-making of ICU shift leaders is a complex multi-professional process, which requires a lot of immediate information. Real-time support for information related to patient admission, the organisation and man¬agement of work, and allocation of staff resources is especially needed. The preliminary information integration model can be applied when real-time enterprise resource planning systems are developed for intensive care daily management