Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are: • Steap learning curve; formal techniques are said to be hard to use. • Lack of a step-by-step construction mechanism and poor guidance. • Difficulty to integrate the technique into the existing software processes. Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML. However, the case of coupling Object-Z (and also Z) and the Use Case Maps (UCMs) notation is still to be explored. A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored. The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software Requirements engineering process. / Computer Science / M. Sc. (Computer Science) / D. Phil. (Computer Science)

No description available.

No description available.

Despite the fact that Sustainable Development (SD) has been growing since the 1980s, methods and models that assist in carrying out sustainable strategies are still uncommon. IT managers at AstraZeneca (AZ) struggle to come up with the most sustainable decision in IT because there are no methods/models that facilitate such a decision-making process at AZ. This thesis aims at evaluating newly suggested sustainability additions to the Adaptive Delivery Framework (ADF) by comparing them to the Green Design (GD) (a model for sustainable decision-making of capital investment projects at AZ) and the Analytical Hierarchy Process (AHP). The evaluation was done using quantitative and qualitative methods. The quantitative method utilized a method from previous research that employs pair-wise comparisons and matrix multiplication, and the qualitative method was in the form of one-on-one semi-structured interviews with AstraZeneca employees. The results showed that the new ADF performed sufficiently well against the already established GD and the literature’s state-of-the-art AHP. The new additions to ADF are capable of dealing with the sustainability problems of IT. Furthermore, the results from the quantitative and the qualitative methods suggested that the additions could improve in three key areas, namely the interdisciplinary approach, long-term perspective, and participation. First, the interdisciplinary approach could be improved by including the indirect and transformational effects of IT. Second, the long-term perspective could be improved by incorporating some long-term assessments, such as the expected number of uses, expected data access proportion, and the expected lifetime. Third, the participation could be improved by including a facilitator during the URS meetings. / Trots att hållbar utveckling SD har vuxit sedan dess 1980-talet, metoder och modeller som hjälper till att genomföra hållbara strategier är fortfarande ovanliga. IT-chefer på AstraZeneca (AZ) kämpar för att komma upp med det mest hållbara beslutet inom IT eftersom det inte finns några metoder/modeller som underlättar en sådan beslutsprocess på AZ. Denna avhandling syftar till utvärderar nyligen föreslagna hållbarhetstillägg till Adaptive Delivery Framework (ADF) genom att jämföra dem med Green Design (GD) (en modell för hållbart beslutsfattande av kapitalinvesteringsprojekt på AZ) och den Analytical Hierarchy Process (AHP). Utvärderingen gjordes med hjälp av kvantitativa och kvalitativa metoder. Den kvantitativa metoden använde en metod från tidigare forskning som använder parvisa jämförelser och matrismultiplikation, och den kvalitativa metoden var i form av en- semistrukturerade intervjuer med AstraZeneca anställda. Resultaten visade att den nya ADF:en fungerade tillräckligt bra mot den redan etablerade GD och litteraturens toppmoderna AHP. De nya tilläggen till ADF är kapabla att hantera hållbarhetsproblemen inom IT. Dessutom, resultaten från de kvantitativa och kvalitativa metoderna antydde det tilläggen skulle kunna förbättras inom tre nyckelområden, nämligen det tvärvetenskapliga förhållningssätt, långsiktighet och delaktighet. Först det tvärvetenskapliga tillvägagångssätt skulle kunna förbättras genom att inkludera indirekta och transformerande effekter av IT. För det andra skulle det långsiktiga perspektivet kunna förbättras genom att införliva vissa långsiktiga bedömningar, såsom det förväntade antalet användningar, förväntas dataåtkomstandel och förväntad livslängd. För det tredje, deltagandet skulle kunna förbättras genom att inkludera en facilitator under URS-mötena.

Student mobility in the area of Higher Education (HE) is gaining more attention nowadays. It is one of the cornerstones of the Bologna Process being promoted at both national and international levels. However, currently there is no technical system that would support student mobility processes and assist users in authoring educational curricula involving student mobility. In this study, the problem of student mobility programmes generation based on existing modules and programmes is considered. A similar problem is being solved in an Intelligent Tutoring Systems field using Curriculum generation techniques, but the student mobility area has a set of characteristics limiting their application to the considered problem. One of main limiting factors is that mobility programmes should be developed in an environment with heterogeneous regulations. In this environment, various established routines and regulations are used to control different aspects of the educational process. These regulations can be different in different domains and are supported by different authors independently. In this thesis, a novel framework was developed for generation of student mobility programmes in an environment with heterogeneous regulations. Two core technologies that were coherently combined in the framework are hierarchical planning and policy-based management. The policy-based planner was designed as a central engine for the framework. It extends the functionality of existing planning technologies and provides the means to carry out planning in environments with heterogeneous regulations, specified as policies. The policy-based planner enforces the policies during the planning and guarantees that the resultant plan is conformant with all policies applicable to it. The policies can be supported by different authors independently. Using them, policy authors can specify additional constraints on the execution of planning actions and extend the pre-specified task networks. Policies are enforced during the planning in a coordinated manner: situations when a policy can be enforced are defined by its scope, and the outcomes of policy evaluation are processed according to the specially defined procedures. For solving the problem of student mobility programme generation using the policy-based planner, the planning environment describing the student mobility problem area was designed and this problem was formalised as a planning task. Educational processes valid throughout the HE environment were formalised using Hierarchical Task Network planning constructs. Different mobility schemas were encoded as decomposition methods that can be combined to construct complex mobility scenarios satisfying the user requirements. New mobility programmes are developed as detailed educational processes carried out when students study according to these programmes. This provides the means to model their execution in the planning environment and guarantee that all relevant requirements are checked. The postponed policy enforcement mechanism was developed as an extension of the policy-based planner in order to improve the planning performance. In this mechanism, future dead-ends can be detected earlier during the planning using partial policy requests. The partial policy requests and an algorithm for their evaluation were introduced to examine policies for planning actions that should be executed in the future course of planning. The postponed policy enforcement mechanism was applied to the mobility programme generation problem within the descending policy evaluation technique. This technique was designed to optimise the process of programme components selection. Using it, policies for different domains can be evaluated independently in a descending order, gradually limiting the scope for the required component selection. The prototype of student mobility programme generation solution was developed. Two case studies were used to examine the process of student mobility programmes development and to analyse the role of policies in this process. Additionally, four series of experiments were carried out to analyse performance gains of the descending policy evaluation technique in planning environments with different characteristics.

In the mid 1990s a previous prohibitions against multi-story buildings higher than two floors with a wooden frame was changed. Today multi-storey buildings are being built in Skellefteå, Sundsvall, Växjö, and Stockholm with others. Despite this only one of five houses being built today has a wooden frame. Since the municipality is a key force to get projects with wooden frames, this papers purpose is to improve tender document for the opportunity to submit bids and building with wooden frames. To help us forward with our work three questions were formulated. 1) What is the basis from a wooden constructions company perspective, of which they determines if they can place a bid or not? 2) What is the difference between tender documents made by a municipality compared to a private buyer? 3) How can tender documents be improved to create an opportunity to place a bid containing an alternative frame system? To answer these questions a literature study was carried out. The literature study is the basis of this paper. To obtain empirical data a document analysis of tender documents was carried out. The result of the study shows that wood frames are hard to adapt to an already finished technical specification, or to a tender document containing an extensive technical specification. To obtain alternative solutions, the buyer should focus on object design, form and function, or a general technical specification. Instead the technical specifications should be drawn up by the supplier, or in collaboration with them. The tender evaluation should be made by the most economically advantageous rather then the lowest price. Then the buyer can evaluate the offers against each other, rather then choosing the lowest price. This also gives the possibility for suppliers to make a bid containing an alternative solution. As a continuation of this paper, we recommend a study on which impact a general technical specification has on the project final cost.  Furthermore a study exploring which possibilities partner procurement can have alternative solutions in the Swedish procurement act. This report deal exclusively with how tender documents should be formulated. Life cycle analysis, carbon dioxide emissions and strength calculations will not be executed.

In recent years, there has been a flood of continuously changing information from a variety of web resources such as web databases, web sites, web services and programs. Online Social Networks (OSNs) represent such a field where huge amounts of information are being posted online over time. Due to the nature of OSNs, which offer a productive source for qualitative and quantitative personal information, researchers from various disciplines contribute to developing methods for extracting data from OSNs. However, there is limited research which addresses extracting data automatically. To the best of the author's knowledge, there is no research which focuses on tracking the real time changes of information retrieved from OSN profiles over time and this motivated the present work. This thesis presents different approaches for automated Data Extraction (DE) from OSN: crawler, parser, Multi Agent System (MAS) and Application Programming Interface (API). Initially, a parser was implemented as a centralized system to traverse the OSN graph and extract the profile's attributes and list of friends from Myspace, the top OSN at that time, by parsing the Myspace profiles and extracting the relevant tokens from the parsed HTML source files. A Breadth First Search (BFS) algorithm was used to travel across the generated OSN friendship graph in order to select the next profile for parsing. The approach was implemented and tested on two types of friends: top friends and all friends. In case of top friends, 500 seed profiles have been visited; 298 public profiles were parsed to get 2197 top friends' profiles and 2747 friendship edges, while in case of all friends, 250 public profiles have been parsed to extract 10,196 friends' profiles and 17,223 friendship edges. This approach has two main limitations. The system is designed as a centralized system that controlled and retrieved information of each user's profile just once. This means that the extraction process will stop if the system fails to process one of the profiles; either the seed profile (first profile to be crawled) or its friends. To overcome this problem, an Online Social Network Retrieval System (OSNRS) is proposed to decentralize the DE process from OSN through using MAS. The novelty of OSNRS is its ability to monitor profiles continuously over time. The second challenge is that the parser had to be modified to cope with changes in the profiles' structure. To overcome this problem, the proposed OSNRS is improved through use of an API tool to enable OSNRS agents to obtain the required fields of an OSN profile despite modifications in the representation of the profile's source web pages. The experimental work shows that using API and MAS simplifies and speeds up the process of tracking a profile's history. It also helps security personnel, parents, guardians, social workers and marketers in understanding the dynamic behaviour of OSN users. This thesis proposes solutions for web database processing on data extraction from OSNs by the use of parser and MAS and discusses the limitations and improvements.

Automating the generation of test cases for software is an active area of research. Specification based test generation is an approach in which a formal representation of a method is analyzed to generate valid test cases. Constraint solving and state space exploration are important aspects of the specification based test generation. One problem with specification based testing is that the size of the state space explodes when we apply this approach to a code of practical size. Hence finding ways to reduce the number of candidates to explore within the state space is important to make this approach practical in industry. Korat is a tool which generates test cases for Java programs based on predicates that validate the inputs to the method. Various ongoing researches intend to increase the tools effectiveness in handling large state space. Parallelizing Korat and minimizing the exploration of invalid candidates are the active research directions. This report surveys the basic algorithms of Korat, PKorat, and Fast Korat. PKorat is a parallel version of Korat and aims to take advantage of multi-processor and multicore systems available. Fast Korat implements four optimizations which reduce the number of candidate explored to generate validate candidates and reduce the amount of time required to explore each candidate. This report also presents the execution time results for generating test candidates for binary tree, doubly linked list, and sorted singly linked list, from their respective predicates. / text

Dans cette thèse on présente une proposition pour la spécification de protocoles de communication utilisés dans le contexte de systèmes multiagent, et qui nous appelons basée sur rôles. L'idée de rôle est récurrente dans le domaine de systèmes multiagent, et représente ce qui fait un agent dans une organisation, c'est à dire, la fonctionnalité qui est accomplie par l'agent dans le système, fonctionnalité qui est exprimée très souvent sous la forme d'échanges de messages qui suivent un protocole o séquence predéfinie. En nous centrant exclusivement sur l'aspect de l'interaction, il est possible d'abstraire la fonctionnalité du système en termes de séquences de messages stéréotypées. Séquences qui peuvent être utilisées comme un méthode de spécification en choisissant une notation appropriée. Nous proposons ici un processus de traduction à partir d'une notation visuelle inspirée de la proposition AUML, qui peut représenter le processus de communication dans un système multiagent, et le traduire vers une représentation formelle en Promela pour effectuer sa validation.

本篇論文論證在漢語中動詞以及文獻中所認定的形容詞(putative adjectives)之間的區分是非必要的。本文探討了文獻中區分和辨別漢語形容詞詞類的各項準則，並論證這些準則並無法全面性解釋所有傳統上被視為是形容詞的詞彙，也因此使得漢語語法更加複雜和歧異。文獻中所認定的形容詞在句法上並未呈現出形容詞的特性；相反地，它們無論是從時貌標記來看或就範疇功能(categorial function)等方面而論都與動詞一致。因此，把文獻中所認定的形容詞與動詞歸於一類將可維持漢語語法的簡單性。 此外，我們認為Chomsky (1965)以兩個正負號特徵(±N, ±V)所界定出的四個詞類(名詞、動詞、形容詞以及介係詞)並不是普遍性的(universal)；意即，並非所有語言都需要同時擁有這四個詞類。功能語言學派的看法亦同，他們認為語言中最少只需要兩個詞類來執行語言功能，即動詞與名詞，因此只有這兩個詞類具有普遍性，而另兩個詞類的語意功能可藉由它們來執行。對此，我們引用了缺乏形容詞(如：韓語(cf. Kim 2002a, 2002b))及介係詞(如：賽德克語(cf. Huang 1998))語言的語料來佐證只有動詞與名詞具有普遍性的看法。最後，本文採用Bhat (1994)在觀察跨語言間形容詞詞類的行為表現後所提出的形容詞鑑定標準，來證明漢語中並沒有一個獨立的形容詞詞類。 / This thesis argues that the verb-adjective distinction in Mandarin Chinese is unnecessary. The criteria for identifying a distinct adjectival category have been proposed by many linguists, e.g., Zhu (1982), Yin (2003), Huang et al (2008); however, they fail to accommodate all putative adjectives as a category. A distinct adjective category requires stipulations to account for the verb-adjective distinction and thus complicates the grammar. Descriptively, putative adjectives in Mandarin Chinese do not exhibit adjectival characteristics; rather, they are unmarked predicates and thus behave similarly as verbs in terms of aspectual marking, N’-ellipsis, and reduplication. Putative adjectives should thus be conflated with verbs to maintain the simplicity of the grammar. From a typological perspective, some languages have been argued to lack adjectives (e.g., Korean (cf. Kim 2002)) and others, prepositions (e.g., Seediq (cf. Huang 1998)). Therefore, Chomsky’s (1965) four categories defined by two universal feature specifications [±N] and [±V] do not seem to be ubiquitous. Functionalist linguists also assert that only Noun and Verb are universal, for they represent the elementary and central concepts at two extremes of the world while Adjective and Preposition may not be syntactically realized and their semantic concepts are thus associated with either Noun or Verb. Finally, Chinese putative adjectives are further examined with the cross-linguistic criteria proposed in Bhat (1994). The only logical conclusion is that Mandarin Chinese does not distinguish adjectives as a distinct category.