In this master thesis we investigated whether it is possible to use automatically generated C code from Function Block Diagram models as an input to the CPAchecker model checker in order to generate automated test cases. Function Block Diagram is a non-executable programming and modeling language. Consequently, we need to transform this language to an executable language that can be model checked. A tool that achieves this is the MITRAC tool, a proprietary development tool used in the embedded system domain, for engineering programmable logic controllers. The purpose of this research was to investigate to what extent the generated C code using MITRAC can be reused as an input to the CPAchecker tool for automated test case generation. In order to achieve this we needed to perform certain transformations steps on the existing code. In addition, necessary instrumentations were needed in order to trigger CPAtiger, an extension of CPAchecker which generates test cases, to achieve maximum condition coverage. We showed that by performing the required modifications it is feasible to reuse the generated C code as an input to CPAchecker tool. We also showed an approach for mapping the generated test cases with the actual Function Block Diagram. We performed mutation analysis in order to evaluate the quality of the generated test cases in terms of the number of injected faults they detect. Test case generation with CPAchecker could be improved in the future in terms of reducing the number of transformations and instrumentations that are currently needed. In order to achieve this we need to add to CPAchecker tool support for structures that are used in C, such as structs. Finally we can extend the type of logic coverage criteria we can use with CPAchecker by adding additional support of FQL language.

Recent advances in test automation have seen a host of new techniques for automated test generation, which traditionally has largely been a manual and expensive process. These techniques have enabled generation of much larger numbers of tests at a much reduced cost. When executed successfully, these tests enable a significant increase in our confidence in the program's correctness. However, as our ability to generate greater numbers of tests increases, we are faced with the problem of the likely high cost of executing all the tests in terms of the total execution time. This thesis presents a novel approach - clustered test execution - to address this problem. Instead of executing each test case separately, we execute parts of several tests using a single execution, which then forks into several directions as the behaviors of the tests differ. Our insight is that in a large test suite, several tests are likely to have common initial execution segments, which do not have to be executed over and over again; rather such a segment could be executed once and the execution result shared across all those tests. As an enabling technology we use the Java PathFinder(JPF) model checker, which is a popular explicit-state model checker for Java programs. Experimental results show that our clustering approach for test execution using JPF provides speed-ups over executing each test in turn from a test suite on the JPF java virtual machine. / text

A UML é uma notação gráfica utilizada na modelagem de sistemas orientados a objetos, em diferentes domínios da computação. Por ser simples de utilizar, em relação a outras formas de modelagem, a UML é amplamente difundida entre os desenvolvedores de software, tanto na academia quanto na indústria. Entre as suas vantagens, encontram-se: (i) a representação visual das relações entre classes e entidades, pois ao se utilizar de diagramas, a UML facilita o entendimento e a visualização das relações dentro do sistema modelado; (ii) a legibilidade e usabilidade, sem que seja necessário a leitura do código do sistema, uma vez que um desenvolvedor pode compreender quais partes do código são redundantes ou reutilizadas; e (iii) uma ferramenta de planejamento, ao auxiliar na definição do que deve ser feito, antes que a implementação comece de fato, além de poder produzir código e reduzir o tempo de desenvolvimento. Todavia, a UML possui desvantagens, tais como: (i) ambiguidade entre elementos UML diferentes, devido a sobreposição dos diagramas; e (ii) falta de uma semântica clara, o qual geralmente faz com que a semântica da linguagem de programação seja adotada. Para mitigar essas desvantagens, pesquisadores buscam atribuir uma semântica formal à UML. Esse tipo de semântica é encontrado em modelos formais, onde o sistema modelado é livre de ambiguidades e possui uma semântica clara e precisa. Por sua vez, os modelos formais não são simples de serem criados e compreendidos por desenvolvedores. O grau de conhecimento em formalismo necessário para utilizar tal modelo é alto, o que faz com que seu uso seja menos difundido, comparado com a notação gráfica não formal da UML. Apesar dos esforços dos pesquisadores, as técnicas de formalização semântica da UML apresentam, no geral, um problema pouco abordado: apesar de utilizar a UML para modelar o sistema, o artefato final dessas técnicas é um trace formal. Considerando o conhecimento comum de um desenvolvedor de software, esse trace dificulta a análise dos problemas, encontrados pelos model checkers, e a correção dos mesmos no modelo UML. Com o objetivo de auxiliar o desenvolvedor na compreensão dos resultados formais (o trace citado), esta tese de doutorado apresenta uma abordagem baseada em Model-driven Architecture (MDA) capaz de representar as informações dos resultados formais dentro de um modelo UML. Por meio de transformações do modelo UML, essas representações, definidas utilizando a abordagem, auxiliam o desenvolvedor a visualizar o fluxo de execução do model checker dentro do modelo UML. Assim, acredita-se que as vantagens obtidas pela formalização semântica da UML podem ser mais difundidas e utilizadas pelos desenvolvedores, principalmente na indústria. / UML is a graphical notation used for modeling object-oriented software systems in different domains in computer science. Being simple to use, compared to other modeling techniques, UML is widespread among software developers, both in academia and industry. Among its advantages are: (i) the visual representation of the relationships between classes and entities, as when using diagrams, UML facilitates understanding and visualization of relationships within the modeled system; (ii) readability and usability without having to read the system code, since a developer can understand which parts of the code are redundant or reusable; and (iii) a planning tool, helping to define what needs to be done before the implementation actually begins, as well as being able to produce code and reduce development time. However, the UML also has disadvantages, such as: (i) ambiguity between different UML elements due to overlapping diagrams; and (ii) lack of clear semantics, which generally causes the semantics of the programming language to be adopted. To mitigate these disadvantages, researchers seek to assign a formal semantics to the UML. This type of semantics is found in formal models, where the modeled system is free of ambiguity and has a clear and precise semantics. On the other hand, formal models are not simple to create and understand by developers. The degree of formalism knowledge required to use such a model is high, which makes their use less widespread, compared to UML non-formal graphical notation. Despite the researchers efforts, in general the techniques that formalize the UML semantics has a problem that is forgotten: although using the UML to model the system, the final artifact of these techniques is a formal trace. Considering the common knowledge of a software developer, this trace makes it difficult to analyze the problems encountered by model checkers and to correct them in the UML model. In order to assist the developer in understanding the formal results (the trace above), this thesis presents an approach based on Model-driven Architecture (MDA) capable of representing the information of the formal results in the UML model. Through UML model transformations, these representations, set using the approach, help the developer to visualize the execution flow of the model checker within the UML model. Thus, we believe that the advantages obtained by formalizing the UML semantics may be more widespread and used by developers, especially in industry.

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um software quando exercitadas. Apesar destas duas características, as principais técnicas de verificação, teste de software e verificação formal, e as ferramentas a elas vinculadas, tendem a negligenciar o comportamento excepcional. Alguns dos fatores que levam a esta negligência são a não especificação do comportamento excepcional em termos de projeto e a consequente implementação das estruturas de tratamento com base no julgamento individual de cada programador. Isto resulta na não consideração de partes expressivas do código em termos de verificação e, consequentemente, a possibilidade de não serem detectados erros relativos tanto às próprias estruturas de tratamento quanto às estruturas de código vinculadas a estas. A fim de abordar este problema, propomos uma técnica, baseada em model checking, que automatiza o processo de exercício de caminhos excepcionais. Isto permite que seja observado o comportamento de um software quando da ocorrência de uma exceção. Pretendemos, com esta técnica, dar suporte para que seja aplicado aos caminhos que representam o comportamento excepcional de um software as mesmas técnicas de detecção de erros que são aplicadas aos caminhos que representam o comportamento normal e, com isso, agregar um aumento na qualidade do desenvolvimento de software. / Software developed in modern languages, such as Java, commonly present structures of exception handling. These structures, when exercised, may affect the software behavior. Despite these two characteristics, the main verification techniques, software testing and formal verification and the tools related to them, tend to neglect the exceptional behavior. The nonexistent specification of software exceptional behaviors at the design level, and, the subsequent implementation of exception handling based on the judgment of each programmer, are some factors that lead to this neglect. These factors result in the non-consideration of the expressive parts of the code in verification terms and, consequently, the impossibility of errors detection concerning either the exception treatment structures or the code structures linked to them. Taking this fact into consideration, we propose a technique based on the model checking process, which automates the process of exercising exceptional paths to address this problem. This allows the observation of the software behavior when an exception occurs. With this technique, we intend to support the application of the same error detection techniques for program normal behavior paths to the paths that represent the software exceptional behavior. Therefore, using the proposed technique, we aim to increase the software development quality.

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um software quando exercitadas. Apesar destas duas características, as principais técnicas de verificação, teste de software e verificação formal, e as ferramentas a elas vinculadas, tendem a negligenciar o comportamento excepcional. Alguns dos fatores que levam a esta negligência são a não especificação do comportamento excepcional em termos de projeto e a consequente implementação das estruturas de tratamento com base no julgamento individual de cada programador. Isto resulta na não consideração de partes expressivas do código em termos de verificação e, consequentemente, a possibilidade de não serem detectados erros relativos tanto às próprias estruturas de tratamento quanto às estruturas de código vinculadas a estas. A fim de abordar este problema, propomos uma técnica, baseada em model checking, que automatiza o processo de exercício de caminhos excepcionais. Isto permite que seja observado o comportamento de um software quando da ocorrência de uma exceção. Pretendemos, com esta técnica, dar suporte para que seja aplicado aos caminhos que representam o comportamento excepcional de um software as mesmas técnicas de detecção de erros que são aplicadas aos caminhos que representam o comportamento normal e, com isso, agregar um aumento na qualidade do desenvolvimento de software. / Software developed in modern languages, such as Java, commonly present structures of exception handling. These structures, when exercised, may affect the software behavior. Despite these two characteristics, the main verification techniques, software testing and formal verification and the tools related to them, tend to neglect the exceptional behavior. The nonexistent specification of software exceptional behaviors at the design level, and, the subsequent implementation of exception handling based on the judgment of each programmer, are some factors that lead to this neglect. These factors result in the non-consideration of the expressive parts of the code in verification terms and, consequently, the impossibility of errors detection concerning either the exception treatment structures or the code structures linked to them. Taking this fact into consideration, we propose a technique based on the model checking process, which automates the process of exercising exceptional paths to address this problem. This allows the observation of the software behavior when an exception occurs. With this technique, we intend to support the application of the same error detection techniques for program normal behavior paths to the paths that represent the software exceptional behavior. Therefore, using the proposed technique, we aim to increase the software development quality.

A UML é uma notação gráfica utilizada na modelagem de sistemas orientados a objetos, em diferentes domínios da computação. Por ser simples de utilizar, em relação a outras formas de modelagem, a UML é amplamente difundida entre os desenvolvedores de software, tanto na academia quanto na indústria. Entre as suas vantagens, encontram-se: (i) a representação visual das relações entre classes e entidades, pois ao se utilizar de diagramas, a UML facilita o entendimento e a visualização das relações dentro do sistema modelado; (ii) a legibilidade e usabilidade, sem que seja necessário a leitura do código do sistema, uma vez que um desenvolvedor pode compreender quais partes do código são redundantes ou reutilizadas; e (iii) uma ferramenta de planejamento, ao auxiliar na definição do que deve ser feito, antes que a implementação comece de fato, além de poder produzir código e reduzir o tempo de desenvolvimento. Todavia, a UML possui desvantagens, tais como: (i) ambiguidade entre elementos UML diferentes, devido a sobreposição dos diagramas; e (ii) falta de uma semântica clara, o qual geralmente faz com que a semântica da linguagem de programação seja adotada. Para mitigar essas desvantagens, pesquisadores buscam atribuir uma semântica formal à UML. Esse tipo de semântica é encontrado em modelos formais, onde o sistema modelado é livre de ambiguidades e possui uma semântica clara e precisa. Por sua vez, os modelos formais não são simples de serem criados e compreendidos por desenvolvedores. O grau de conhecimento em formalismo necessário para utilizar tal modelo é alto, o que faz com que seu uso seja menos difundido, comparado com a notação gráfica não formal da UML. Apesar dos esforços dos pesquisadores, as técnicas de formalização semântica da UML apresentam, no geral, um problema pouco abordado: apesar de utilizar a UML para modelar o sistema, o artefato final dessas técnicas é um trace formal. Considerando o conhecimento comum de um desenvolvedor de software, esse trace dificulta a análise dos problemas, encontrados pelos model checkers, e a correção dos mesmos no modelo UML. Com o objetivo de auxiliar o desenvolvedor na compreensão dos resultados formais (o trace citado), esta tese de doutorado apresenta uma abordagem baseada em Model-driven Architecture (MDA) capaz de representar as informações dos resultados formais dentro de um modelo UML. Por meio de transformações do modelo UML, essas representações, definidas utilizando a abordagem, auxiliam o desenvolvedor a visualizar o fluxo de execução do model checker dentro do modelo UML. Assim, acredita-se que as vantagens obtidas pela formalização semântica da UML podem ser mais difundidas e utilizadas pelos desenvolvedores, principalmente na indústria. / UML is a graphical notation used for modeling object-oriented software systems in different domains in computer science. Being simple to use, compared to other modeling techniques, UML is widespread among software developers, both in academia and industry. Among its advantages are: (i) the visual representation of the relationships between classes and entities, as when using diagrams, UML facilitates understanding and visualization of relationships within the modeled system; (ii) readability and usability without having to read the system code, since a developer can understand which parts of the code are redundant or reusable; and (iii) a planning tool, helping to define what needs to be done before the implementation actually begins, as well as being able to produce code and reduce development time. However, the UML also has disadvantages, such as: (i) ambiguity between different UML elements due to overlapping diagrams; and (ii) lack of clear semantics, which generally causes the semantics of the programming language to be adopted. To mitigate these disadvantages, researchers seek to assign a formal semantics to the UML. This type of semantics is found in formal models, where the modeled system is free of ambiguity and has a clear and precise semantics. On the other hand, formal models are not simple to create and understand by developers. The degree of formalism knowledge required to use such a model is high, which makes their use less widespread, compared to UML non-formal graphical notation. Despite the researchers efforts, in general the techniques that formalize the UML semantics has a problem that is forgotten: although using the UML to model the system, the final artifact of these techniques is a formal trace. Considering the common knowledge of a software developer, this trace makes it difficult to analyze the problems encountered by model checkers and to correct them in the UML model. In order to assist the developer in understanding the formal results (the trace above), this thesis presents an approach based on Model-driven Architecture (MDA) capable of representing the information of the formal results in the UML model. Through UML model transformations, these representations, set using the approach, help the developer to visualize the execution flow of the model checker within the UML model. Thus, we believe that the advantages obtained by formalizing the UML semantics may be more widespread and used by developers, especially in industry.

The building industry are currently going through a huge alteration. The introduction of BIM (Building Information Modeling). Which also implements a lot of new ways of solving problems that building modeling can cause. This report is written for Uppsala University in cooperation with Temagruppen in Uppsala. However, it contains a comparison between two different systems that checks building models. Temagruppen invested in a new Swedish adaptation of a software called Solibri Model Checker. This Software controlling the availability in building models, it also introduces a new way of interaction between different instances during a building project. The definition of the report is availability in public buildings. A building model has been designed in Revit, then imported to Solibri Model Checker who controls the availability and creates a report of certain design fault. Interviews are given to get a look into how the work with availability controls currently works at Temagurppuen. This results in a discussion of benefits and disadvantages of the two different methods. The result finally shows that certain work can be more effectively done with Solibri Model Checker. But availability contains more than just disabled impairment. Visual- and cognitive impairment can’t still be controlled by just a computer software.

BIM är en fras som har tagits upp allt frekventare inom byggbranschen senaste åren. Uttrycket har olika innebörd beroende på vem som tillfrågas och dennes kunskap inom området. BIM-verktyg är något som med åren också har ökat på marknaden. Verktygen har olika användningsområden beroende på vilken aktör som ska utnyttja det. I BIM-projekt används såkallade samordningsverktyg för att bland annat kontrollera olika discipliners modeller där valet av programvara är avgörande beroende på funktionalitet och nyttjare.  I detta arbete studerades två programvaror som kan användas vid BIM-samordning. Genom en fallstudie har det undersökts vilket utav programvarorna Autodesk Navisworks Manage 2015 och Solibri Model Checker 9.5 som passar bäst för Grontmij AB i Eskilstuna efter deras behov och förutsättningar. Efter en grundlig studie av båda programvarorna påvisar rapporten att den rekommenderade programvaran specifikt för Grontmij AB i Eskilstuna är Solibri Model Checker 9.5 i enlighet med företagets behov och förutsättningar. / BIM is a phrase that has been raised increasingly frequent in the construction industry in recent years. The term has different meanings depending on who is asked. BIM tools is something that over the years also has increased on the market. The tools have different use depending on the user. Bim projects use so-called coordination tools for including control of various disciplines models where the choice of software is different, depending on functionality and users. This thesis addresses two software programs that can be used in BIM coordination. Through a case study, the author investigated which of the softwares Autodesk Navisworks Manage 2015 and Solibri Model Checker 9.5 is best for Grontmij AB in Eskilstuna to their needs and circumstances.

Att utföra kostnadskalkyler och mängdavtagningar utifrån objektbaserade 3D-modeller har visat sig vara problematiskt då modellerna inte uppfyller de förväntade kraven på informationsnivå. De bristande modellerna leder till en större osäkerhet då kalkylatorn skall upprätta kostnadskalkyler, vilket utgör bakgrunden till de frågeställningar som rapporten utgörs av. Projektet Biomedicum, som skall bli det toppmoderna laboratoriet åt Karolinska Institutet bedrivs som ett fullskaligt BIM-projekt, där de objektbaserade 3D-modellerna utgör underlaget för bland annat kostnadskalkyler i systemhandlingsskedet. Kalkylatorn i projektet, har uttryckt ett missnöje gällande kvaliteten i modellerna, och menar på att det finns stora brister som leder till att risken för att osäkra kalkyler upprättas ökar. Denna rapport kommer således att se över hur det är möjligt att kvalitetssäkra en objektbaserad 3D-modell i IFC-format i programvaran Solibri Model Checker, utifrån de projektspecifika kraven som råder i projektet. Rapporten utgörs av en fallstudie och en litteraturstudie, och till viss del även av intervjuer. I fallstudien undersöks det om Solibri Model Checker är kapabel till att kontrollera modellerna utifrån de projektspecifika krav som råder i projektet, samt att analysera resultatet av kontrollerna som har utförts. Intervjuerna i sin tur har legat till grund för ett antal problem som har ansetts vara relevanta för rapporten. Problem som kan härledas till juridiska svårigheter, avsaknad av en gemensam branschstandard, meningsskiljaktigheter kring innehållet i en objektbaserad 3D-modell etc.  I fallstudien har det visat sig att 3D-modellerna är bristande ur kalkylsynpunkt. Detta leder till svårigheter och osäkerheter då Skanska upprättar kalkylerna. Anledningarna till detta är flera. Det handlar bland annat om att konstruktören använder sig av en modelleringsteknik som inte är anpassad för kalkylering, men även att det inte finns tydliga riktlinjer om vilken information som bör finnas i objekten i systemhandlingsskedet, vilket har framgått under intervjuerna. Det har även framgått under intervjuerna, att ett avgörande problem som kan anknytas till att modellerna är av bristande kvalitet ur kalkylsynpunkt, är på grund av att det inte har ställts krav tillräckligt tidigt i processen. Vad som är viktigt för att få en fungerande process där de objektbaserade 3D-modellerna skall användas för mängdavtagningar och kostnadskalkyler, är att i ett tidigt skede fastslå vilken information som behövs i objekten för att trovärdiga kalkyler skall vara möjliga att upprätta. Vikten av att det finns en tydlig IT-handledning är även stor, då det är handledningen som ligger till underlag om vilken information som skall finnas med i modellerna. / To perform quantity takeoffs and cost estimates based on 3D models is problematic, if the models do not meet the expected demands of information. The weaknesses of the models leads to uncertainty when the calculator will establish cost estimates, which forms the background to the issues that the thesis constitutes. The project Biomedicum is conducted as a full-fledged BIM project, where the object based 3D models are the basis for cost estimates in the system phase. The calculator in the project has expressed dissatisfaction regarding the quality of the models, and believes that there are major flaws that lead to the risk of uncertain calculations increasing. Of this reason, this thesis will analyze the possibilities about ensuring the quality of an object based 3D model in IFC format, by using the software Solibri Model Checker. This thesis consists of a literature review, interviews and a case study. The case study examines whether Solibri Model Checker is capable of checking the models based on the project specific requirements, and to analyze the results of the checks that have carried out in the case study. The interviews have been the basis for the number of problems that have been considered relevant for the thesis. Problems that can be traced to legal difficulties, lack of a common set requirements, disagreements about the content of an object based 3D model etc. The case study has shown that the 3D models are inadequate to perform cost estimates, which leads to difficulties and uncertainties in the calculation process. There are several reasons for this. The designers of the project have used wrong modeling technique for quantity takeoff and cost estimating. But also that there are no clear guidelines as to what information should be included in the items in the document stage system, which has emerged during the interviews. It has also emerged during the interviews that crucial problems that may be linked to the models are of poor quality, because it has not been required early enough in the process. What is important to get a working process in which the object-based 3D models to be used for quantity takeoffs and cost estimates, is that in the early stages determine what information is needed in the objects to credible estimates will be possible to establish. The importance of a clear IT manual is also great, as it is the manual who serves as the basis of the information to be included in the models.

Idag tillämpas BIM (Building Information Modeling) som ett ledande verktyg inom byggprojektering och möjliggör lösningar som är hållbara och optimerade mellan olika discipliner för att effektivt hantera informationsflöden. Vid överföring av data mellan programvaror används ett neutralt filformat, IFC (Industry Foundation Classes). Detta filformat exporteras från 3Dmodelleringsprogrammet Tekla Structures. Syftet med detta examensarbete är att granska orsaken till saknad information vid IFC-export från Tekla Structures. Studien innefattar en fallstudie, komparativ studie samt intervjuer. I fallstudien studeras inställningarna för en IFC-export från en komplex modell i Tekla Structures. Den komparativa studien berör två samordningsprogram Solibri Model Checker och Navisworks Manage, som sedan ställs mot varandra. Det som undersöks är hur IFC-filer lämpar sig i samordningsprogrammen. Intervjuerna har legat till grund och har gett tydliga riktlinjer under arbetets gång. Resultatet av denna studie tyder på att orsakerna kring saknad information i IFC-filer är den mänskliga faktorn och bristande kunskaper av inställningarna i en IFC-export. Ytterligare resultat är jämförelsen mellan samordningsprogrammen som visar att båda är lämpade för IFC-formatet. Genom den komparativa studien har det visat att Solibri lämpar sig bättre för IFC-exporter från Tekla Structures. Med hänsyn till examensarbetets resultat är den mänskliga faktorn avgörande för informationsförluster. Den mänskliga faktorn utgör att det råder bristande kommunikation samt bristande kunskap om IFC-exporter. / Today, BIM (Building Information Modeling) is applied as a leading tool in structural design and modeling and enables solutions that are sustainable and optimized between different disciplines to effectively manage information flows. In connection with transfers between software’s a neutral file format, IFC (Industry Foundation Classes), is used. This file format is exported from the 3D-modeling program Tekla Structures. The purpose of this thesis is to examine the reason for missing information on IFC exports from Tekla Structures. The study includes a case study, comparative study and interviews In the case study, the settings for an IFC- export are studied from a complex 3D- model in Tekla Structures. The comparative study concerns two coordination programs Solibri Model Checker and Navisworks Manage, which are compared against each other. What is examined is how IFC- files are suitable in the coordination programs. The interviews have given clear guidelines during the work. The results indicate that the causes of missing information in IFC -files are the human factor and the lack of knowledge of the settings of an IFC- export. Additional to the results that was achieved are the comparison between the coordination programs shows that both programs are suitable for the IFCformat. The difference between the coordination programs is how one of them signalized the format better than the other Regarding the results, the human factor is crucial for the information loss. The human factor has shown that the lack of communication and knowledge of IFC- exports is a reason for the information loss. Through the comparative study, it has also been shown that Solibri is better suited for IFCexports from Tekla Structures.