The growing use of computers in modern control systems has led to the develop- ment of complex dynamic systems known as hybrid systems, which integrates both discrete and continuous systems. Given that hybrid systems are systems that operates in real time allowing for changes in continuous state over time periods, and discrete state changes across zero time, their modelling, analysis and verification becomes very difficult. The formal verifications of such systems based on specifications that can guar- antee their behaviour is very important especially as it pertains to safety critical applications. Accordingly, addressing such verifications issues are important and is the focus of this thesis. In this thesis, in order to actualise the specification and verification of hybrid systems, Interval Temporal Logic(ITL) was adopted as the underlying formalism given its inherent characteristics of providing methods that are flexible for both propositional and first-order reasoning regarding periods found in hardware and software system’s descriptions. Given that an interval specifies the behaviour of a system, specifications of such systems are therefore represented as a set of intervals that can be used to gain an understanding of the possible behaviour of the system in terms of its composition whether in sequential or parallel form. ITL is a powerful tool that can handle both forms of composition given that it offers very strong and extensive proof and specification techniques to decipher essential system properties including safety, liveliness and time projections. However, a limitation of ITL is that the intervals within its framework are considered to be a sequence of discrete states. Against this back- drop, the current research provides an extension to ITL with the view to deal with verification and other related issues that centres around hybrid systems. The novelty within this new proposition is new logic termed SPLINE Interval Temporal Logic (SPITL) in which not only a discrete behaviour can be expressed, but also a continuous behaviour can be represented in the form of a spline i.e. the interval is considered to be a sequence of continuous phases instead of a sequence of discrete states. The syntax and semantics of the newly developed SPITL are provided in this thesis and the new extension of the interval temporal logic using a hybrid system as a case study. The overall framework adopted for the overall structure of SPITL is based on three fundamental steps namely the formal specification of hybrid systems is expressed in SPLINE Interval Temporal Logic, followed by the executable subset of ITL, called Tempura, which is used to develop and test a hybrid system specification that is written in SPITL and finally a runtime verification tool for ITL called AnaTempura which is linked with Matlab in order to use them as an integrated tool for the verification of hybrid systems specification. Overall, the current work contributes to the growing body of knowledge in hybrid systems based on the following three major milestones namely: i. the proposition of a new logic termed SPITL; ii. executable subset, Tempura, integrated with SPITL specification for hybrid systems; and iii. the development of a tool termed Ana Tempura which is integrated with Matlab to ensure accurate runtime verification of results.

Test-driven development (TDD) has been the target of many articles in which the authors try to reveal the impact of TDD compared to the traditional iterative test-last approach (ITL). Most of the existing articles conducts case studies in academic setting or in industrial setting with focus on metrics of little relevance for the industry. The metrics Defect Density per 1000 lines of code (DD/KLOC) and McCabe’s cyclomatic complexity number are frequently used to show differences between ITL and TDD in quality. However, these metrics are outdated and irrelevant in today’s industry according to several articles regarding TDD. The reason is the introduction of high-level programming languages such as Java, C# and Python. To compare these languages with assembler languages is not feasible. In this master thesis, the author suggests measuring defect density per hour instead (DD/h) of per 1000 lines of code to establish the quality and success of a software project. DD/h together with total hours needed to develop the software is a better measurement and is not dependent on programming language and complexity as DD/KLOC is to describe quality and the scope of the development project. By examine DD/h from five case studies comparing ITL and TDD the author shows a possible positive change in quality and resources needed in software development projects. / Testdriven utveckling (TDD) har varit i fokus många artiklar där författarna försöker kartlägga TDD: s inverkan jämfört med det traditionella tillvägagångssättet där tester körs sist i utvecklingsprocessen (ITL). De flesta av de befintliga artiklarna genomför fallstudier i akademisk miljö eller i industriella miljöer med fokus på mätvärden som saknar relevans för industrin. Defektdensitet per 1000 linjer kod (DD/KLOC) och McCabes cyklomatiska komplexitetsnummer används ofta för att visa skillnader mellan ITL och TDD i kvalitet. Dessa mätvärden är emellertid föråldrade och irrelevanta i dagens bransch enligt flera akademiska artiklar. Anledningen är introduktionen av programmeringsspråk så som Java, C #och Python. Att jämföra dessa språk med assembler-språk är inte möjligt. I detta examensarbete föreslår författaren att man mäter defektendensitet per timme (DD/h) istället för DD/KLOC för att fastställa kvaliteten för ett mjukvaruprojekt. DD/h tillsammans med de totala timmar som behövs för att utveckla programvaran är ett bättre mätvärde och är inte beroende av programmeringsspråk och komplexitet som DD/KLOC är för att beskriva kvaliteten och omfattningen av utvecklingsprojektet. Genom att undersöka DD/h från fem fallstudier som jämför ITL och TDD visar författaren en möjlig positiv förändring av kvalitet och resurser som behövs för att genomföra ett mjukvaruutvecklingsprojekt.

The aim of this study is to investigate four teachers’ ideas and experiences of Information and Computer Technologies (ICT) in the early years of learning to read in the lower grades of school. This is done with the aid of qualitative interviews. The results of the interviews are then discussed on the basis of Vygotsky’s sociocultural theory. The informants work in three different municipalities in southern Sweden. The study presents research that is both positive and negative to the use of computers or tablets instead of pen and paper in the teaching of writing. The study also aims to elucidate the informants’ perception of advantages and disadvantages of ICT in teaching. The result shows that the informants have a positive view of ICT as a complement in their teaching. The informants, however, are limited by external factors such as access to technical tools and Internet connections, which causes frustration and has the effect that they get relatively little actual experience of it. The teacher’s technical competence and the age of the pupils also affect the working methods and the pupils’ assignments. / Syftet med den här studien är att undersöka fyra lärares föreställningar om och erfarenheter av IKT i den tidiga läsinlärningen, för skolans yngre årskurser. Detta görs med hjälp av kvalitativa intervjuer. Resultatet från intervjuerna diskuteras sedan utifrån Vygotskijs sociokulturella teori. Informanterna arbetar i tre olika kommuner i södra Sverige. I studien presenteras forskning som är både positiv och negativ till att använda dator eller surfplatta istället för penna och papper i skrivundervisningen. Studien syftar även till att belysa informanternas upplevda för- och nackdelar med IKT i undervisningen. Resultatet visar att informanterna är positivt inställda till IKT som ett komplement i undervisningen. Informanterna begränsas dock av yttre faktorer som tillgång på tekniska verktyg och internetuppkoppling, vilket dels skapar frustrationer, dels leder till att deras erfarenheter är förhållandevis få. Även lärarens tekniska kompetens och elevernas ålder påverkar arbetssätt och uppgifter.