1 |
Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral ModelsFilipovikj, Predrag January 2017 (has links)
Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. This trend impacts all phases of the system development including requirements specification, design and architecture of the system, as well as the integration and testing phases. In such settings, creating and managing different artifacts during the system development process by using traditional, human-intensive techniques becomes increasingly difficult. One problem stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints. Another problem is related to the fact that industrial development relies on models, e.g. developed in Simulink, from which code may be generated, so the correctness of such models needs to be ensured. A potential way to address of the mentioned problems is by applying computer-aided specification, analysis and verification techniques already at the requirements stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of formal specification and analysis techniques, their integration with industrial practice remains a challenge. To address this challenge, in this thesis, we develop the foundation of a framework, tailored for industrial adoption, for formal specification and analysis of system requirements specifications and behavioral system models. First, we study the expressiveness of existing pattern-based techniques for creating formal requirements specifications, on a relevant industrial case study. Next, in order to enable practitioners to create formal system specification by using pattern-based techniques, we propose a tool called SeSAMM Specifier. Further, we provide an automated Satisfiability Modulo Theories (SMT)-based consistency analysis approach for the formally encoded system requirements specifications. The proposed SMT-based approach is suitable for early phases of the development for debugging the specifications. For the formal analysis of behavioral models, we provide an approach for statistical model checking of Simulink models by using the UPPAAL SMC tool. To facilitate the adoption of the approach, we provide the SIMPPAAL tool that automates procedure of generating network of stochastic timed automata for a given Simulink model. For validation, we apply our approach on a complex industrial model, namely the Brake-by-Wire function from Volvo GTT. / VeriSpec
|
2 |
Transformando modelos Scade em especificações SCRSERAFIM, Kamila Nayana Carvalho 08 September 2016 (has links)
Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-08-08T13:40:24Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5) / Made available in DSpace on 2017-08-08T13:40:24Z (GMT). No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5)
Previous issue date: 2016-09-08 / A construção de um software para domínios particulares tem de atender normas específicasque impõem o atendimento a fatores como rastreabilidade de requisitos e certificação. Por exemplo, a indústria aeronáutica deve atender à norma DO-178B que estabelece restrições para uso de software de aeronaves, que são considerados sistemas críticos. Para um sistema estar de acordo com essa certificação é necessário ter requisitos formais e código certificado; nesta direção, Andrade (ANDRADE, 2013) usou a notação SCR (Software Cost Reduction) para definição de requisitos e a ferramenta SCADE para modelagem de sistemas críticos, com desenvolvimento de um tradutor de SCR para artefatos xscade. A prática de desenvolvimento de sistema, porém, não está restrita à transição entre requisitos e artefatos de projeto. Modificações realizadas nestes últimos devem também ser refletidas nos requisitos. Neste trabalho desenvolvemos um tradutor de artefatos de modelagem da ferramenta SCADE para SCR. Desta forma podemos gerar especificação de requisitos a partir do código (Engenharia Reversa) e complementamos o trabalho anterior desenvolvido por Andrade (ANDRADE, 2013). Para o desenvolvimento do tradutor, utilizamos a plataforma Spoofax por meio da qual descrevemos a sintaxe do esquema XML utilizado em SCADE e também as regras de tradução tendo como alvo SCR. A validação da tradução teve como ponto de partida o resultado do uso do tradutor desenvolvido por Andrade (ANDRADE, 2013), tendo de gerar como saída a mesma entrada do tradutor desenvolvido por Andrade (ANDRADE, 2013). Além disso, desenvolvemos exemplos para demonstrar que a modificação estrutural, com preservação de semântica, em projetos SCADE, é verificável por meio do uso de testes gerados por meio da ferramenta TTM-TVEC / Building a software for particular domains must attend specific standards that impose
attendance to factors such as traceability requirements and the certification issue. For
example, the airline industry should meet the DO-178B standard that establishes restrictions
on the use of aircraft software, which is considered a critical system. For a system to
be in accordance with this certification, one must have formal requirements and certified
code. In this direction, Andrade (ANDRADE, 2013) used SCR (Software Cost Reduction)
for requirements definition and SCADE for modeling critical systems with development of
an artifacts a translator from SCR. However the practice of developing is not restricted
to the transition from requirements to design artifacts. Changes made on design should
be reflected in the requirements. In this work we developed a translator from SCADE
to SCR. In this way we can generate requirements specification from the code (reverse
engineering) and complement the previous Andrade (ANDRADE, 2013) thesis. For the
translator development, we use the Spoofax platform through which we describe the XML
schema syntax used in SCADE and also the translation rules having SCR as the target
language. The translation validation had as its starting point the result of the translator
developed by Andrade (ANDRADE, 2013), where the output is the same input developed
by Andrade(ANDRADE, 2013). Furthermore, examples developed to demonstrate that
the structural modification that preserves semantics in SCADE, is verifiable through the
use of tests generated by the TTM-TVEC tool.
|
3 |
Digitala testamenten : Behöver formkraven för upprättande av testamente moderniseras? / Digital wills : Are the formal requirements for establishing a will in need of a modernization?Jigler Envall, Annika January 2014 (has links)
Genom ett testamente kan en person se till så att han får sin yttersta vilja fram efter hans bortgång. Vid upprättande av testamente måste dock en testator ta hänsyn till de formkrav som gäller för handlingen, vilka är kraven på skriftlighet, underskrift och bevittning. Dessa formkrav brukar traditionellt sett bestå av en fysisk del, så som att testamentet ska upprättas på papper, testatorn ska egenhändigt skriva under testamentet och bevittningen ska ske genom fysisk närvaro. Vi lever dock i ett allt mer digitaliserat och teknikvänligt samhälle och en naturlig följd av det vore om en person kunde upprätta ett digitalt testamente. Syftet med denna uppsats är att fastställa gällande rätt avseende testamentets formkrav och utreda om de kan uppfyllas genom ett digitalt testamente. Eftersom formkraven inte kan uppfyllas elektroniskt traditionellt sett, kommer författaren istället att utgå ifrån syftena bakom formkraven. Bakom kravet på skriftlighet ligger främst bevis- och äkthetsfunktionen som syftar till att säkerställa ett testamentes tillblivelse, giltighet och innehåll. Kravet på underskrift grundas främst på viljeförklaringsfunktionen, med andra ord att testatorn ska intyga om att testamentet utgör hans yttersta vilja. Kravet på bevittning syftar till att kunna säkerställa testamentets legala upprättande och underskriftens äkthet. Syftena bakom kraven på skriftlighet, underskrift och bevittning kan uppfyllas även vid användning av elektroniska rutiner. Dock finns inte idag den teknik som behövs för att spara och arkivera elektroniskt underskrivna handlingar under en längre period. Därmed kan inte ordinära testamenten upprättas i digital form, medan holografiska testamenten som bara är giltiga i tre månader borde kunna upprättas digitalt. / Through a will, a person can make sure that he gets his last wishes taken care of after his death. When establishing a will, however, you have to take into account the formal requirements of the act, such as that the will have to be in writing, signed and witnessed. These procedural requirements traditionally consist of a physical part, for example the will shall be written on paper, the testator must personally sign the will and the witnessing shall be achieved through physical presence. However, we live in an increasingly digitized and technology-oriented society and the natural consequence of this would be if a person could establish a digital will. The purpose of this paper is to determine the applicable law in respect of the formal requirements of a will and investigate whether they can be met by a digital will. Since the formal requirements can not traditionally be met electronically, the author will instead look at the underlying aims of the formal requirements. Behind the requirement of writing is primarily the evidence and authenticity feature which aims to ensure the wills creation, validity and content. The requirement of signature is based primarily on the intent function, in other words, the testator must certify that the will contains his last wishes. The requirement of witnessing aims to ensure the wills legal establishment and signature authenticity. The purposes behind the requirements of writing, signed and witnessing can be met even when using electronic procedures. However, the technology available today is not able to save and archive electronically signed documents for a longer period. Because of this ordinary wills cannot be drawn up in digital form, whereas holographic wills, that are only valid for three months, should be able to be drawn up in digital form.
|
4 |
Le consentement à la convention d'arbitrage commercial international : évolution et développement récents en droit québécois et en droit internationalKost de Sèvres, Nicolette 12 1900 (has links)
"Mémoire présenté à la Faculté des études supérieures en vue de l'obtention du grade de LL.M. en droit option droit des affaires" / L'arbitrage évolue parallèlement et en accord au développement du commerce et des
relations internationales s'accompagnant d'un accroissement des différends
commerciaux de plus en plus complexes et spécialisés. En choisissant l'arbitrage, les
parties excluent, de manière consensuelle, la compétence juridictionnelle des tribunaux
étatiques. Ce droit à l'accès aux tribunaux étatiques se retrouve notamment à la Charte
québécoise des droits et libertés de la personne. La validité d'une convention
d'arbitrage dépend donc avant tout de la preuve de son existence et la preuve du
consentement des parties s'y rattachant. La nécessité de l'écrit est donc un moyen de
s'assurer du consentement des parties. La Convention de New York de 1958 énumère
plusieurs de ces principes de forme. Son article 11(2), qui prévoit que la convention
d'arbitrage doit être par écrit, n'est plus adapté aux réalités juridiques et commerciales
d'aujourd'hui ni au développement du commerce électronique. Que peut être considéré
comme un écrit afin de répondre aux exigences de l'article 1I(2)? Abordée par la
CNUDCI, cette problématique quant au formalisme requis dans l'expression de la
volonté des parties à se soumettre à l'arbitrage est d'une importance capitale dans la
mesure des différentes interprétations qui existent à ce sujet tant au niveau du droit
québécois et canadien qu'au niveau du droit international. Une réforme des dispositions
législatives quant au formalisme écrit du consentement à l'arbitrage doit être mise en
place et ce, soit par une réforme des dispositions législatives existantes ou par une mise
à jour officielle de l'interprétation donnée aux dispositions actuelles en vigueur. / Arbitration has evolved in parallel and in accordance with the development of
commerce and of international relations coming along with the rise of commercial
disputes which are becoming increasingly complex and specialised. By choosing
arbitration, the parties consensually exclude the jurisdiction ofState courts. This right to
access State courts is protected namely in the Charter ofHuman Rights and Freedoms.
The validity of an arbitration clause therefore depends above all on the proof of its
existence and of the consent of the parties to that effect. The necessity of the written
form becomes a mean that insures of the consent of the parties. The 1958 New York
Convention enumerates several of those formal requirements. !ts section 11(2), which
states that the arbitration clause has to be in written form, is not adapted to today's legal
and commercial reality nor to the development of electronic commerce. What exactly is
considered as ''written'' in order to respect the requirements of section 1I(2)? As
addressed by UNCITRAL, the issue concerning the formalism required for the
expression of the parties' intent to be subjected to arbitration is of a vital importance.
Numerous interpretations exist in Canadian law as well as in International law. A
reform of the existing legal provisions relating to the consent of arbitration needs to be
implemented, either through a reform of the existing provisions or through an official
process to update the interpretation given to the requirements that are a1ready in place.
|
5 |
La convention d’arbitrage dans le contrat de transport maritime de marchandises : étude comparée des droits français, hellénique et anglais / Arbitration agreement in contracts of carriage of goods by sea : a comparative study of french, greek and english lawPapadatou, Marina 26 May 2014 (has links)
Cette étude porte sur la question de l’efficacité de la convention d’arbitrage à l’égard des opérateurs du transport maritime de marchandises. Dans un premier temps, la question qui se pose est celle de la détermination du droit applicable à l’efficacité de ladite clause. A cet égard, notre attention se concentre sur l’interprétation et l’application des principes propres à l’arbitrage international par la jurisprudence maritime. L’examen des clauses d’arbitrage insérées dans un contrat de transport maritime ne saurait échapper aux spécificités du droit de transport maritime ainsi qu’aux dispositions des conventions maritimes internationales. Par ailleurs, l’approche du sujet par la méthode comparative nous permettra de découvrir, à travers les solutions concrètes finalement retenues dans les trois systèmes juridiques en question, que l’effet juridique de la clause compromissoire est directement lié à l a position contractuelle de ces opérateurs. Parmi les personnes impliquées dans le transport maritime, le destinataire des marchandises nous intéresse plus particulièrement. Ce dernier n’étant pas présent, en effet, au moment de la formation du contrat, les conditions de son engagement par une clause compromissoire insérée, presque toujours « par référence » dans le titre de transport, font l’objet d’un vif débat doctrinal et jurisprudentiel. / This study is primarily focused on the enforceability of arbitration agreements incorporated in contracts of carriage of goods by sea. First, we will cover the important issue of determining the law applicable to these arbitration agreements. Special attention will be given to how courts tend to implement general international arbitration principles to maritime disputes. An arbitration agreement incorporated in acontract of carriage of goods by sea should also be analyzed in light of the specificities of maritime transport law and applicable international shipping conventions. Moreover, the comparative methodology used herein will show that the enforceability of arbitration agreements is closely related to the qualification of the operators involved in the contract. In particular, among the commercial players involved in the carriage of the goods, we sought to examine the legal position of the consignee of the goods. Indeed, since the consignee is absent at the moment of the contract formation, the binding effect there upon of the arbitration agreement, which is generally incorporated “by reference” to the bill of lading, is highly debated by scholars and judges.
|
6 |
Le consentement à la convention d'arbitrage commercial international : évolution et développement récents en droit québécois et en droit internationalKost de Sèvres, Nicolette 12 1900 (has links)
L'arbitrage évolue parallèlement et en accord au développement du commerce et des
relations internationales s'accompagnant d'un accroissement des différends
commerciaux de plus en plus complexes et spécialisés. En choisissant l'arbitrage, les
parties excluent, de manière consensuelle, la compétence juridictionnelle des tribunaux
étatiques. Ce droit à l'accès aux tribunaux étatiques se retrouve notamment à la Charte
québécoise des droits et libertés de la personne. La validité d'une convention
d'arbitrage dépend donc avant tout de la preuve de son existence et la preuve du
consentement des parties s'y rattachant. La nécessité de l'écrit est donc un moyen de
s'assurer du consentement des parties. La Convention de New York de 1958 énumère
plusieurs de ces principes de forme. Son article 11(2), qui prévoit que la convention
d'arbitrage doit être par écrit, n'est plus adapté aux réalités juridiques et commerciales
d'aujourd'hui ni au développement du commerce électronique. Que peut être considéré
comme un écrit afin de répondre aux exigences de l'article 1I(2)? Abordée par la
CNUDCI, cette problématique quant au formalisme requis dans l'expression de la
volonté des parties à se soumettre à l'arbitrage est d'une importance capitale dans la
mesure des différentes interprétations qui existent à ce sujet tant au niveau du droit
québécois et canadien qu'au niveau du droit international. Une réforme des dispositions
législatives quant au formalisme écrit du consentement à l'arbitrage doit être mise en
place et ce, soit par une réforme des dispositions législatives existantes ou par une mise
à jour officielle de l'interprétation donnée aux dispositions actuelles en vigueur. / Arbitration has evolved in parallel and in accordance with the development of
commerce and of international relations coming along with the rise of commercial
disputes which are becoming increasingly complex and specialised. By choosing
arbitration, the parties consensually exclude the jurisdiction ofState courts. This right to
access State courts is protected namely in the Charter ofHuman Rights and Freedoms.
The validity of an arbitration clause therefore depends above all on the proof of its
existence and of the consent of the parties to that effect. The necessity of the written
form becomes a mean that insures of the consent of the parties. The 1958 New York
Convention enumerates several of those formal requirements. !ts section 11(2), which
states that the arbitration clause has to be in written form, is not adapted to today's legal
and commercial reality nor to the development of electronic commerce. What exactly is
considered as ''written'' in order to respect the requirements of section 1I(2)? As
addressed by UNCITRAL, the issue concerning the formalism required for the
expression of the parties' intent to be subjected to arbitration is of a vital importance.
Numerous interpretations exist in Canadian law as well as in International law. A
reform of the existing legal provisions relating to the consent of arbitration needs to be
implemented, either through a reform of the existing provisions or through an official
process to update the interpretation given to the requirements that are a1ready in place. / "Mémoire présenté à la Faculté des études supérieures en vue de l'obtention du grade de LL.M. en droit option droit des affaires"
|
7 |
Styrningens påverkan i börsbolag : En kvalitativ studie om hur långsiktighet beaktas i en småländsk kontextNilsson, Simon, Andersson, Gustav January 2020 (has links)
Bakgrund och problem: Att vara ett börsnoterat bolag innebär en ökad kravbild samtidigt som företaget blir offentligt kan förväntningar från främst aktieägare förhöjas. Fokus mot främst aktieägarna kan i vissa fall leda till att bolaget utgår ifrån ett mer kortsiktigt förhållningssätt, i den mån att skapa värde för ägarna. För att då minimera riskerna att bli kortsiktig, blir vikten av styrning mot långsiktighet en viktig faktor. Det blir därav intressant att undersöka hur börsbolag via sin styrning beaktar distinktionen mellan aktieägarvärde och långsiktighet. Syfte: Studiens syfte är att ge en förklaring till hur styrningen påverkas av att verka i en noterad miljö och hur detta avspeglas i de olika bolagens sätt att styra verksamheten. Studien ämnar att öka kunskapen om hur synen på aktieägarvärde och långsiktighet ter sig och om möjlig hur de båda samordnas i bolagen. Metod: Metoden som valts för studien var en kvalitativ intervjustudie som ansågs vara mest lämplig sett till frågeställningar samt studiens syfte. Den empiriska materialinsamlingen har huvudsakligen skett med hjälp av semistrukturerade intervjuer som har utförts med ledande personer i börsbolagen. Slutsats: Styrningen i börsbolag ändras inte i så stor utsträckning av att verka i en noterad miljö, men det finns tendenser att den blivit mer formaliserad gällande främst rapportering. Den strategiska och taktiska styrningen formas till viss del utifrån börsen formella krav men även till viss del av intressenters kravbild. Samordning mellan långsiktighet och skapande av aktieägarvärde blir viktig för att begränsa kortsiktiga förhållningssätt främst med hjälp av bolagens tydliga strategiska inriktning. Koordineringen sker genom börsbolagens förmåga att tillgodose både aktieägarnas krav och uppnå bolagens långsiktiga planer. / Background and research problem: To be a listed company, it implies an increase in demands and, simultaneously, the expectations from the shareholders can be enhanced. The focus towards the shareholders, could in some cases result in short-sightedness in the company to increase their value. To minimize the risks of short-sightedness, the importance of management control towards long-sightedness becomes a crucial factor. It is thereby interesting to investigate how listed companies, with their management control, considers the distinction between shareholder value and long-sightedness. Purpose: The purpose of this study is to give an explanation of how the management control alters by acting in a listed environment, and how it reflects in the different companies´ ways to control the business. The study intends to increase the knowledge of the view of how shareholder value and long-sightedness appears and, if possible, how these coordinates in the companies. Method: The method that was chosen for the study was a qualitative interview-study, which were considered the most appropriate method aligned to the research questions and the purpose of the study. The empirical material collection has occurred primarily with the aid of semi-structured interviews which have been conducted with senior executives in the listed companies. Conclusion: The management control in listed companies do not change, to a large extent, although there are tendencies that it has become more formalized regarding the reporting. The strategic management and management control are formed, to a certain degree, by the stock exchange´s formal requirements but also, to some degree, the stakeholder’s demands. The coordination between long-sightedness and the creation of shareholder value becomes vital in order to constrain short-term approaches, with the aid of the companies´ clear strategic direction. The coordination occurs by the listed companies’ ability to satisfy both the shareholders demands and accomplish the companies´ long-term plans.
|
8 |
Återkallelse av testamente : Särskilt om bedömningen av om testator har avsett att återkalla sitt testamente / On the Revocation of Wills : Especially regarding the assessment of whether the testator has intended to revoke his willSteen, Johan January 2023 (has links)
In most European legal systems, drafting a will is subject to formal requirements. In the same way, most European legal systems prescribe formal requirements for the revocation of a will. However, Swedish law is unique in this respect as it does not prescribe formal requirements for the revocation of a will. For the revocation of a will, Swedish law only requires that the testator has unequivocally announced that the disposition no longer expresses his ultimate will. This is stated in the 5th Section of the 10th Chapter of the Swedish Inheritance Code. Under Swedish law, it is therefore only a question of proof whether the testator has revoked his will. However, it may be difficult to assess whether the testator has intended to revoke his will when the testator is alleged to have revoked his will informally. Therefore, the main purpose of this thesis is to examine how the assessment of whether the testator has intended to revoke his will is carried out under current Swedish law. To achieve the purpose of this thesis, a traditional legal dogmatic method is used. This means that the material used is limited to the traditional Swedish sources of law. These are legislation, preparatory works, case law and Swedish legal doctrine. Since Swedish law does not prescribe any formal requirements for revoking a will, a will can be revoked in an unlimited number of ways. It has therefore been necessary to limit the scope of this thesis to the most common ways of revoking a will. For this reason, this thesis only covers the revocation of a will by executing a new will, by physical destruction of a will, by strikeouts and inscriptions on the will, by oral statements made by the testator and by the revocation of a previously revoked will. Consequently, other ways of revoking a will are not closer analysed. The analysis shows that no general conclusions can be drawn on how to assess whether the testator intended to revoke his will. Instead, the assessment depends on the way in which the testator is alleged to have revoked his will. However, the analysis also shows that some more specific conclusions can be drawn. It can be concluded from Swedish case-law that a high standard of proof is required for a revocation allegedly made by an informal measure. However, this does not apply if the will has been destructed. In such cases, there is instead a presumption that the will has been destructed by the testator with the purpose of revoking the will. Consequently, the burden of proof is reversed when the will has been destructed. The analysis also shows that it often can be uncertain whether the testator has intended to revoke his will by an informal measure. This is because there may be no reliable evidence of the testator’s intention in such cases. Therefore, the con-clusion is that a testator who wishes to revoke his will should do so by executing a new will which expressly states that the will is revoked. By doing so, the testator significantly reduces the risk of future disputes concerning the validity of the will.
|
Page generated in 0.0726 seconds