You searched for subject:(formal methods).
Showing records 1 – 30 of
417 total matches.
◁ [1] [2] [3] [4] [5] … [14] ▶
Cornell University
1.
Raman, Vasumathi.
Explaining Unsynthesizability Of High-Level Robot Behaviors.
Degree: PhD, Computer Science, 2013, Cornell University
URL: http://hdl.handle.net/1813/34373 
► As robots become increasingly capable and general-purpose, it is desirable for them to be easily controllable by a wide variety of users. The near future…
(more)
▼ As robots become increasingly capable and general-purpose, it is desirable for them to be easily controllable by a wide variety of users. The near future will likely see robots in homes and offices, performing everyday tasks such as fetching coffee and tidying rooms. There is therefore a growing need for non-expert users to be able to easily program robots performing complex high-level tasks. Such high-level tasks include behaviors comprising non-trivial sequences of actions, reacting to external events, and achieving repeated goals. Recent advances in the application of
formal methods to robot control have enabled automated synthesis of correct-by-construction hybrid controllers for complex highlevel tasks. These approaches use a discrete abstraction of the robot workspace and a temporal logic specification of the environment assumptions and desired robot behavior, and yield controllers that are provably correct with respect to this abstraction and specification. However, there are many remaining challenges in ensuring that a user-defined specification yields a robot controller that achieves the desired high-level behavior. This dissertation addresses several causes of failure resulting from logical implications of the specification itself, as well as those arising because of inconsistencies between the discrete abstraction and the continuous execution domain. Work on three main challenges is described. The first is an algorithm for the analysis of logic specifications, which provides a high-level cause of failure for specifications that have no implementation, or unsynthesizable specifications. An interactive game is also introduced, allowing users to explore the cause of unsynthesizability. The second is the identification of a minimal explanation of failure: several techniques are presented to identify a core subset of the specification that causes unsynthesizability. The third problem addressed is the definition of an appropriate timing semantics for ion and execution of hybrid controllers synthesized from high-level specifications. Several controller-synthesis frameworks are compared, and their suitability to different problem domains discussed, based on their underlying assumptions and properties of the resulting continuous behaviors.
Advisors/Committee Members: Kress Gazit, Hadas (chair), Selman, Bart (committee member), Easley, David Alan (committee member), Halpern, Joseph Yehuda (committee member).
Subjects/Keywords: Robotics; Formal Methods; Synthesis
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Raman, V. (2013). Explaining Unsynthesizability Of High-Level Robot Behaviors. (Doctoral Dissertation). Cornell University. Retrieved from http://hdl.handle.net/1813/34373
Chicago Manual of Style (16th Edition):
Raman, Vasumathi. “Explaining Unsynthesizability Of High-Level Robot Behaviors.” 2013. Doctoral Dissertation, Cornell University. Accessed January 18, 2021.
http://hdl.handle.net/1813/34373.
MLA Handbook (7th Edition):
Raman, Vasumathi. “Explaining Unsynthesizability Of High-Level Robot Behaviors.” 2013. Web. 18 Jan 2021.
Vancouver:
Raman V. Explaining Unsynthesizability Of High-Level Robot Behaviors. [Internet] [Doctoral dissertation]. Cornell University; 2013. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/1813/34373.
Council of Science Editors:
Raman V. Explaining Unsynthesizability Of High-Level Robot Behaviors. [Doctoral Dissertation]. Cornell University; 2013. Available from: http://hdl.handle.net/1813/34373
University of Waikato
2.
Liu, Bowen.
Using behavioural specifications to support model-checking
.
Degree: 2019, University of Waikato
URL: http://hdl.handle.net/10289/13028
► Safety-critical interactive systems provide many benefits for human daily life, but erroneous safety-critical interactive systems can lead to serious consequences to the users. Thus building…
(more)
▼ Safety-critical interactive systems provide many benefits for human daily life, but erroneous safety-critical interactive systems can lead to serious consequences to the users. Thus building these systems requires that we ensure a high level of correctness.
Formal models can be used to ensure that safetycritical systems are developed correctly. However, when models of the systems are being built, there is no guarantee that the modelled system fully satisfies the user requirements. If the systems are not what business stakeholders truly desire, new errors can be made. Behaviour-Driven-Development is often applied to ensure the requirements of thesystemareproperlyunderstoodandmaintainedbyusingBehaviouralSpecifications. These specifications use natural language, and so, are well suited for expressing user requirements. They can be used as the basis for test generation but do not provide the guarantees of correctness that
formal methods can provide. In this work, we develop an approach that takes advantage of the expressivity of behaviour specifications and combines it with the use of
formal methods. We use Behavioural Specifications to create First-Order-Logic predicates of the requirements. These predicates can be used with
formal methods, either to support the creation of the
formal models or to ensure the user requirements and specifications are consistent.
Advisors/Committee Members: Bowen, Judy (advisor).
Subjects/Keywords: Formal methods; Cucumber; Behavioural Speficication
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Liu, B. (2019). Using behavioural specifications to support model-checking
. (Masters Thesis). University of Waikato. Retrieved from http://hdl.handle.net/10289/13028
Chicago Manual of Style (16th Edition):
Liu, Bowen. “Using behavioural specifications to support model-checking
.” 2019. Masters Thesis, University of Waikato. Accessed January 18, 2021.
http://hdl.handle.net/10289/13028.
MLA Handbook (7th Edition):
Liu, Bowen. “Using behavioural specifications to support model-checking
.” 2019. Web. 18 Jan 2021.
Vancouver:
Liu B. Using behavioural specifications to support model-checking
. [Internet] [Masters thesis]. University of Waikato; 2019. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10289/13028.
Council of Science Editors:
Liu B. Using behavioural specifications to support model-checking
. [Masters Thesis]. University of Waikato; 2019. Available from: http://hdl.handle.net/10289/13028
University of New South Wales
3.
Cock, David.
Leakage in Trustworthy Systems.
Degree: Computer Science & Engineering, 2014, University of New South Wales
URL: http://handle.unsw.edu.au/1959.4/53707
;
https://unsworks.unsw.edu.au/fapi/datastream/unsworks:12402/SOURCE02?view=true
► This dissertation presents a survey of the theoretical and practical techniques necessary to provably eliminate side-channel leakage through known mechanisms in component-based secure systems.We cover…
(more)
▼ This dissertation presents a survey of the theoretical and practical techniques necessary to provably eliminate side-channel leakage through known mechanisms in component-based secure systems.We cover the state of the art in leakage measures, including both Shannon and min entropy, concluding that Shannon entropy models the observed behaviour of our example systems closely, and can be used to give a safe bound on vulnerability in practical scenarios.We comprehensively analyse several channel-mitigation strategies: cache colouring and instruction-based scheduling, showing that effectiveness and ease of implementation depend strongly on subtle hardware features. We also demonstrate that real-time scheduling can be employed to effectively mitigate remote chan nels at minimal cost.Finally, we demonstrate that we can reason formally (and mechanically) about probabilistic non-functional properties, by formalising the probabilistic language pGCL in the Isabelle/HOL theorem prover, and using it to verify an implementation of lattice scheduling, a well-known cache-channel countermeasure. We prove that a correspondence exists between standard vulnerability bounds, in a channel-centric view, and the refinement lattice on programs in pGCL, used to model a guessing attack on a vulnerable system—a process-centric view.
Advisors/Committee Members: Heiser, Gernot, Computer Science & Engineering, Faculty of Engineering, UNSW.
Subjects/Keywords: Microkernels; Security; Formal methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Cock, D. (2014). Leakage in Trustworthy Systems. (Doctoral Dissertation). University of New South Wales. Retrieved from http://handle.unsw.edu.au/1959.4/53707 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:12402/SOURCE02?view=true
Chicago Manual of Style (16th Edition):
Cock, David. “Leakage in Trustworthy Systems.” 2014. Doctoral Dissertation, University of New South Wales. Accessed January 18, 2021.
http://handle.unsw.edu.au/1959.4/53707 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:12402/SOURCE02?view=true.
MLA Handbook (7th Edition):
Cock, David. “Leakage in Trustworthy Systems.” 2014. Web. 18 Jan 2021.
Vancouver:
Cock D. Leakage in Trustworthy Systems. [Internet] [Doctoral dissertation]. University of New South Wales; 2014. [cited 2021 Jan 18].
Available from: http://handle.unsw.edu.au/1959.4/53707 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:12402/SOURCE02?view=true.
Council of Science Editors:
Cock D. Leakage in Trustworthy Systems. [Doctoral Dissertation]. University of New South Wales; 2014. Available from: http://handle.unsw.edu.au/1959.4/53707 ; https://unsworks.unsw.edu.au/fapi/datastream/unsworks:12402/SOURCE02?view=true
Universidade do Rio Grande do Sul
4.
Barbosa, Raquel de Miranda.
Especificação formal de organizações de sistemas multiagentes.
Degree: 2011, Universidade do Rio Grande do Sul
URL: http://hdl.handle.net/10183/31122
► A abordagem de sistemas multiagentes tem sido cada vez mais utilizada para o desenvolvimento de sistemas complexos, o que despertou o interesse das pesquisas na…
(more)
▼ A abordagem de sistemas multiagentes tem sido cada vez mais utilizada para o desenvolvimento de sistemas complexos, o que despertou o interesse das pesquisas na área de engenharia de software orientada a agentes (AOSE) e modelos organizacionais. Neste contexto, esta tese estuda a aplicabilidade de alguns métodos formais tradicionais de engenharia de software para a especificação formal de organizações de sistemas multiagentes, analisando o uso da linguagem de especificação formal RSL para representar o modelo organizacional PopOrg. A escolha da linguagem RSL ocorreu pelo fato de ela ser uma linguagem de especificação formal que cobre amplo espectro de métodos de especificação formal (baseados em modelos e baseados em propriedades, aplicativos e imperativos, sequenciais e concorrentes) e o modelo PopOrg foi escolhido por ser um modelo mínimo de organização de sistemas multiagentes, concebido para representar o conjunto mínimo de aspectos estruturais e operacionais que tais organizações devem ter. O uso da linguagem RSL foi avaliado tanto para a especificação do aspecto estrutural dos sistemas PopOrg, quanto para especificação operacional desses sistemas. Um estudo preliminar realizado com a linguagem CSP para a especificação operacional do modelo PopOrg também é apresentado, visto que serviu como base para a especificação em RSL. Ao final, apresenta-se uma sugestão de extensão da linguagem RSL para sua maior aplicabilidade à especificação de sistemas multiagentes.
The multiagent systems approach have been increasingly used for the development of complex systems, which aroused the interest of research in Agent Oriented Software Engineering (AOSE) and organizational models. In this context, this thesis studies the applicability of some traditional formal methods of software engineering for the formal specification of multiagent systems organizations, analyzing the use of RSL formal specification language to represent the PopOrg organizational model. The choice of RSL language occurred because it is a formal specification language that covers a wide spectrum of formal specification methods (models-based and properties-based, applicative and imperative, sequential and concurrent) and the PopOrg model was chosen because it is a minimal model of multiagent systems organization, designed to represent the minimum set of structural and operational aspects that such organizations should have. The use of RSL language was evaluated both for specifying the structural aspect of PopOrg systems and the operational specification for these systems. A preliminary study carried out with the CSP language for the operational specification of PopOrg model is also presented, as was the basis for the specification in RSL. In the end, a suggestion is given for an extension of the RSL language, to allow for its wider applicability to the specification of multiagent systems.
Advisors/Committee Members: Costa, Antonio Carlos da Rocha.
Subjects/Keywords: Formal methods; Inteligência artificial; MAS organizations; Sistemas multiagentes; RSL formal specification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Barbosa, R. d. M. (2011). Especificação formal de organizações de sistemas multiagentes. (Thesis). Universidade do Rio Grande do Sul. Retrieved from http://hdl.handle.net/10183/31122
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Barbosa, Raquel de Miranda. “Especificação formal de organizações de sistemas multiagentes.” 2011. Thesis, Universidade do Rio Grande do Sul. Accessed January 18, 2021.
http://hdl.handle.net/10183/31122.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Barbosa, Raquel de Miranda. “Especificação formal de organizações de sistemas multiagentes.” 2011. Web. 18 Jan 2021.
Vancouver:
Barbosa RdM. Especificação formal de organizações de sistemas multiagentes. [Internet] [Thesis]. Universidade do Rio Grande do Sul; 2011. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10183/31122.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Barbosa RdM. Especificação formal de organizações de sistemas multiagentes. [Thesis]. Universidade do Rio Grande do Sul; 2011. Available from: http://hdl.handle.net/10183/31122
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
McMaster University
5.
Kumar, Apurva.
A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain.
Degree: MASc, 2015, McMaster University
URL: http://hdl.handle.net/11375/18416
► Bodies or Books of Knowledge (BoKs) have only been transcribed in mature fields where practices and rules have been well established (settled) and are gathered…
(more)
▼ Bodies or Books of Knowledge (BoKs) have only been transcribed in mature fields
where practices and rules have been well established (settled) and are gathered for
any prospective or current practitioner to refer to. As a precursor to creating a BoK,
it is first important to know if the domain contains settled knowledge and how this
knowledge can be isolated? One approach, as described in this work, is to use Formal
Concept Analysis (FCA) to structure the knowledge (or parts of it) and construct
a pruned concept lattice to highlight patterns of use and filter out the common and
established practices that best suit the solving of a problem within the domain.
In the railway domain, formal methods have been applied for a number of years to
solve various modelling and verification problems. Their common use and straightforward
application (with some refinement) makes them easy to identify and therefore a
prime candidate to test for settled knowledge within the railway domain. They also
provide other assurances of settled knowledge along the way.
Thesis
Master of Applied Science (MASc)
Advisors/Committee Members: Maibaum, Thomas, Gruner, Stefan, Computing and Software.
Subjects/Keywords: Formal Methods; Railway Software; Formal Concept Analysis; Body of Knowledge
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Kumar, A. (2015). A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain. (Masters Thesis). McMaster University. Retrieved from http://hdl.handle.net/11375/18416
Chicago Manual of Style (16th Edition):
Kumar, Apurva. “A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain.” 2015. Masters Thesis, McMaster University. Accessed January 18, 2021.
http://hdl.handle.net/11375/18416.
MLA Handbook (7th Edition):
Kumar, Apurva. “A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain.” 2015. Web. 18 Jan 2021.
Vancouver:
Kumar A. A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain. [Internet] [Masters thesis]. McMaster University; 2015. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/11375/18416.
Council of Science Editors:
Kumar A. A Preparatory Study Towards a Body of Knowledge in the Field of Formal Methods for the Railway Domain. [Masters Thesis]. McMaster University; 2015. Available from: http://hdl.handle.net/11375/18416
Cornell University
6.
Xu, Bingxin.
Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown.
Degree: M.S., Mechanical Engineering, Mechanical Engineering, 2013, Cornell University
URL: http://hdl.handle.net/1813/33823
► This thesis presents the development of high-level guaranteed robot control for reactive behaviours by relaxing two assumptions: 1) the workspace is well-known in advance; 2)…
(more)
▼ This thesis presents the development of high-level guaranteed robot control for reactive behaviours by relaxing two assumptions: 1) the workspace is well-known in advance; 2) the temporal logic based formalisms encode the specification by expressing the properties of future paths. This paper addresses the challenges of relaxing both of the assumptions by presenting an approach for automatically re-synthesizing a hybrid controller that guarantees user-defined high-level robot behaviour while exploring and updating a partially unknown workspace, and providing a concise grammar for specifying highlevel tasks that require memory of past events. In the first challenge, this thesis introduces an approach that includes dynamically adding new regions into the workspace during execution, automatically rewriting the specification, and re-synthesizing the controller while preserving the robot state and its history of task completion. The approach is implemented within the LTLMoP toolkit and is demonstrated in an experiment. For the second challenge, this thesis introduces an innovative structured English grammar for specifying high-level behaviour that automatically performs memory operations without requiring explicit definition from the specification designer. This grammar admits intuitive, unambiguous specifications for tasks that implicitly use memory for purposes including non-repeated goals, strictly ordered requirements, etc. The approach is also implemented within the LTLMoP toolkit.
Advisors/Committee Members: Kress Gazit, Hadas (chair), Hencey, Brandon M. (committee member).
Subjects/Keywords: high-level control; robot; formal methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Xu, B. (2013). Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown. (Masters Thesis). Cornell University. Retrieved from http://hdl.handle.net/1813/33823
Chicago Manual of Style (16th Edition):
Xu, Bingxin. “Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown.” 2013. Masters Thesis, Cornell University. Accessed January 18, 2021.
http://hdl.handle.net/1813/33823.
MLA Handbook (7th Edition):
Xu, Bingxin. “Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown.” 2013. Web. 18 Jan 2021.
Vancouver:
Xu B. Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown. [Internet] [Masters thesis]. Cornell University; 2013. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/1813/33823.
Council of Science Editors:
Xu B. Guaranteeing High-Level Robot Behaviours With Past Memory And Future Unknown. [Masters Thesis]. Cornell University; 2013. Available from: http://hdl.handle.net/1813/33823
University of Waikato
7.
Crickett, Scott.
Design Patterns: Infrastructure and Examples
.
Degree: 2017, University of Waikato
URL: http://hdl.handle.net/10289/11703
► Modern interactive systems can be incredibly complex, with a variety of screens, menus, widgets, etc. available to the user. Due to this, modelling these interactive…
(more)
▼ Modern interactive systems can be incredibly complex, with a variety of screens, menus, widgets, etc. available to the user. Due to this, modelling these interactive systems can also be incredibly complex and while there are techniques to help overcome this, it can often lead to radically different models depending on the modeller.
This thesis explores the use of two design patterns created in order to help simplify modelling interactive systems. In the process of doing this, we first explore µ-Charts and its semantics, which are defined in Z, in order to understand its capabilities. We then discover a feature we name the Return feature, which we break down into two parts, Return Home and Return Back, and create patterns in order to concisely model them. Finally, we test these patterns and evaluate the tools we used to create the µ-charts, translate them into their Z semantics and test them.
Advisors/Committee Members: Reeves, Steve (advisor).
Subjects/Keywords: Computer Science;
Formal Methods;
Design Patterns
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Crickett, S. (2017). Design Patterns: Infrastructure and Examples
. (Masters Thesis). University of Waikato. Retrieved from http://hdl.handle.net/10289/11703
Chicago Manual of Style (16th Edition):
Crickett, Scott. “Design Patterns: Infrastructure and Examples
.” 2017. Masters Thesis, University of Waikato. Accessed January 18, 2021.
http://hdl.handle.net/10289/11703.
MLA Handbook (7th Edition):
Crickett, Scott. “Design Patterns: Infrastructure and Examples
.” 2017. Web. 18 Jan 2021.
Vancouver:
Crickett S. Design Patterns: Infrastructure and Examples
. [Internet] [Masters thesis]. University of Waikato; 2017. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10289/11703.
Council of Science Editors:
Crickett S. Design Patterns: Infrastructure and Examples
. [Masters Thesis]. University of Waikato; 2017. Available from: http://hdl.handle.net/10289/11703
University of Illinois – Urbana-Champaign
8.
Katelman, Michael.
A meta-language for functional verification.
Degree: PhD, 0112, 2012, University of Illinois – Urbana-Champaign
URL: http://hdl.handle.net/2142/29614
► This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the…
(more)
▼ This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the search for a proof within a theorem prover. The programmatic coordination of simulation is difficult with existing tools for digital circuit verification because stimuli generation, simulation execution, and analysis of simulation results are all decoupled. A new programming language to address this problem, analogous to the mechanism for orchestrating proof search tactics within a theorem prover, is defined wherein device simulation is made a first-class notion. This meta-language for functional verification is first formalized in a parametric way over hardware description languages using rewriting logic, and subsequently a more richly featured software tool for Verilog designs, implemented as an embedded domain-specific language in Haskell, is described and used to demonstrate the novelty of the programming language and to conduct two case studies. Additionally, three hardware description languages are given
formal semantics using rewriting logic and we demonstrate the use of executable rewriting logic tools to formally analyze devices implemented in those languages.
Advisors/Committee Members: Meseguer, Jos?? (advisor), Arvind (committee member), Rosu, Grigore (committee member), Torrellas, Josep (committee member).
Subjects/Keywords: Programming Languages; Formal Methods; Hardware Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Katelman, M. (2012). A meta-language for functional verification. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/29614
Chicago Manual of Style (16th Edition):
Katelman, Michael. “A meta-language for functional verification.” 2012. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed January 18, 2021.
http://hdl.handle.net/2142/29614.
MLA Handbook (7th Edition):
Katelman, Michael. “A meta-language for functional verification.” 2012. Web. 18 Jan 2021.
Vancouver:
Katelman M. A meta-language for functional verification. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2012. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/2142/29614.
Council of Science Editors:
Katelman M. A meta-language for functional verification. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2012. Available from: http://hdl.handle.net/2142/29614
Clemson University
9.
Smith, Hampton.
Engineering Specifications and Mathematics for Verified Software.
Degree: PhD, Computer Science, 2013, Clemson University
URL: https://tigerprints.clemson.edu/all_dissertations/1132
► Developing a verifying compiler – a compiler that proves that components are correct with respect to their specifications – is a grand challenge for the computing community.…
(more)
▼ Developing a verifying compiler – a compiler that proves that components are correct with respect to their specifications – is a grand challenge for the computing community. The prevailing view of the software engineering community is that this problem is necessarily difficult because, to-date, the resultant verification conditions necessary to prove software correctness have required powerful automated provers and deep mathematical insight to dispatch. This seems counter-intuitive, however, since human programmers only rarely resort to deep mathematics to assure themselves that their code works. In this work, we show that well-specified and well-engineered software supported by a flexible, extensible mathematical system can yield verification conditions that are sufficiently straightforward to be dispatched by a minimalist rewrite prover. We explore techniques for making such a system both powerful and user-friendly, and for tuning an automated prover to the verification task. In addition to influencing the design of our own system, RESOLVE, this exploration benefits the greater verification community by informing specification and theory design and encouraging greater integration between nuanced mathematical systems and powerful programming languages. This dissertation presents the design and an implementation of a minimalist rewrite prover tuned for the software verification task. It supports the prover with the design and implementation of a flexible, extensible mathematical system suitable for use with an industrial-strength programming language. This system is employed within a well-integrated specification framework. The dissertation validates the central thesis that verification conditions for well-engineered software can be dispatched easily by applying these tools and
methods to a number of benchmark components and collecting and analyzing the resulting data.
Advisors/Committee Members: Sitaraman, Murali, Dean , Brian C, Hallstrom , Jason O, Pargas , Roy P.
Subjects/Keywords: Formal Methods; Specficiation; Verification; Computer Sciences
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Smith, H. (2013). Engineering Specifications and Mathematics for Verified Software. (Doctoral Dissertation). Clemson University. Retrieved from https://tigerprints.clemson.edu/all_dissertations/1132
Chicago Manual of Style (16th Edition):
Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Doctoral Dissertation, Clemson University. Accessed January 18, 2021.
https://tigerprints.clemson.edu/all_dissertations/1132.
MLA Handbook (7th Edition):
Smith, Hampton. “Engineering Specifications and Mathematics for Verified Software.” 2013. Web. 18 Jan 2021.
Vancouver:
Smith H. Engineering Specifications and Mathematics for Verified Software. [Internet] [Doctoral dissertation]. Clemson University; 2013. [cited 2021 Jan 18].
Available from: https://tigerprints.clemson.edu/all_dissertations/1132.
Council of Science Editors:
Smith H. Engineering Specifications and Mathematics for Verified Software. [Doctoral Dissertation]. Clemson University; 2013. Available from: https://tigerprints.clemson.edu/all_dissertations/1132
Kansas State University
10.
Zhang, Zhi.
A formal
approach to contract verification for high-integrity
applications.
Degree: PhD, Department of Computing and
Information Sciences, 2016, Kansas State University
URL: http://hdl.handle.net/2097/32880
► High-integrity applications are safety- and security-critical applications developed for a variety of critical tasks. The correctness of these applications must be thoroughly tested or formally…
(more)
▼ High-integrity applications are safety- and
security-critical applications developed for a variety of critical
tasks. The correctness of these applications must be thoroughly
tested or formally verified to ensure their reliability and
robustness. The major properties to be verified for the correctness
of applications include: (1) functional properties, capturing the
expected behaviors of a software, (2) dataflow property, tracking
data dependency and preventing secret data from leaking to the
public, and (3) robustness property, the ability of a program to
deal with errors during execution.
This dissertation presents and
explores
formal verification and proof technique, a promising
technique using rigorous mathematical
methods, to verify critical
applications from the above three aspects. Our research is carried
out in the context of SPARK, a programming language designed for
development of safety- and security-critical applications.
First,
we have formalized in the Coq proof assistant the dynamic semantics
for a significant subset of the SPARK 2014 language, which includes
run-time checks as an integral part of the language, as any
formal
methods for program specification and verification depend on the
unambiguous semantics of the language.
Second, we have formally
defined and proved the correctness of run-time checks generation
and optimization based on SPARK reference semantics, and have built
the certifying tools within the mechanized proof infrastructure to
certify the run-time checks inserted by the GNAT compiler frontend
to guarantee the absence of run-time errors.
Third, we have
proposed a language-based information security policy framework and
the associated enforcement algorithm, which is proved to be sound
with respect to the formalized program semantics. We have shown how
the policy framework can be integrated into SPARK 2014 for more
advanced information security analysis.
Advisors/Committee Members: John M. Hatcliff.
Subjects/Keywords: Formal
Methods; Language
Semantics; Program
Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zhang, Z. (2016). A formal
approach to contract verification for high-integrity
applications. (Doctoral Dissertation). Kansas State University. Retrieved from http://hdl.handle.net/2097/32880
Chicago Manual of Style (16th Edition):
Zhang, Zhi. “A formal
approach to contract verification for high-integrity
applications.” 2016. Doctoral Dissertation, Kansas State University. Accessed January 18, 2021.
http://hdl.handle.net/2097/32880.
MLA Handbook (7th Edition):
Zhang, Zhi. “A formal
approach to contract verification for high-integrity
applications.” 2016. Web. 18 Jan 2021.
Vancouver:
Zhang Z. A formal
approach to contract verification for high-integrity
applications. [Internet] [Doctoral dissertation]. Kansas State University; 2016. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/2097/32880.
Council of Science Editors:
Zhang Z. A formal
approach to contract verification for high-integrity
applications. [Doctoral Dissertation]. Kansas State University; 2016. Available from: http://hdl.handle.net/2097/32880
Loughborough University
11.
Roslan, Rosmira.
Formal transformation methods for automated fault tree generation from UML diagrams.
Degree: PhD, 2019, Loughborough University
URL: https://doi.org/10.26174/thesis.lboro.11638011.v1
;
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.799192
► With a growing complexity in safety critical systems, engaging Systems Engineering with System Safety Engineering as early as possible in the system life cycle becomes…
(more)
▼ With a growing complexity in safety critical systems, engaging Systems Engineering with System Safety Engineering as early as possible in the system life cycle becomes ever more important to ensure system safety during system development. Assessing the safety and reliability of system architectural design at the early stage of the system life cycle can bring value to system design by identifying safety issues earlier and maintaining safety traceability throughout the design phase. However, this is not a trivial task and can require upfront investment. Automated transformation from system architecture models to system safety and reliability models offers a potential solution. However, existing methods lack of formal basis. This can potentially lead to unreliable results. Without a formal basis, Fault Tree Analysis of a system, for example, even if performed concurrently with system design may not ensure all safety critical aspects of the design.
Subjects/Keywords: Formal transformation methods; Fault Tree; UML Diagrams
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Roslan, R. (2019). Formal transformation methods for automated fault tree generation from UML diagrams. (Doctoral Dissertation). Loughborough University. Retrieved from https://doi.org/10.26174/thesis.lboro.11638011.v1 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.799192
Chicago Manual of Style (16th Edition):
Roslan, Rosmira. “Formal transformation methods for automated fault tree generation from UML diagrams.” 2019. Doctoral Dissertation, Loughborough University. Accessed January 18, 2021.
https://doi.org/10.26174/thesis.lboro.11638011.v1 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.799192.
MLA Handbook (7th Edition):
Roslan, Rosmira. “Formal transformation methods for automated fault tree generation from UML diagrams.” 2019. Web. 18 Jan 2021.
Vancouver:
Roslan R. Formal transformation methods for automated fault tree generation from UML diagrams. [Internet] [Doctoral dissertation]. Loughborough University; 2019. [cited 2021 Jan 18].
Available from: https://doi.org/10.26174/thesis.lboro.11638011.v1 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.799192.
Council of Science Editors:
Roslan R. Formal transformation methods for automated fault tree generation from UML diagrams. [Doctoral Dissertation]. Loughborough University; 2019. Available from: https://doi.org/10.26174/thesis.lboro.11638011.v1 ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.799192
University of Texas – Austin
12.
Yang, Hongkun.
Efficient verification of packet networks.
Degree: PhD, Computer science, 2015, University of Texas – Austin
URL: http://hdl.handle.net/2152/33271
► Network management will benefit from automated tools based upon formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying…
(more)
▼ Network management will benefit from automated tools based upon
formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying network properties in the data plane. This dissertation presents efficient algorithms for computing reachability and verifying network properties for a single network with both packet filters and transformers, and for interconnected networks.
For computing port to port reachability in a network, we present a new
formal method for a new tool, Atomic Predicates (AP) Verifier, which is much more time and space efficient than existing tools. Given a set of predicates representing packet filters, AP Verifier computes a set of atomic predicates, which is minimum and unique. The use of atomic predicates dramatically speeds up computation of network reachability. AP Verifier also includes algorithms to process network update events and check compliance with network policies and properties in real time.
Packet transformers are widely used in Internet service provider networks, datacenter infrastructures, and layer-2 networks. Existing network verification tools do not scale to such networks with large numbers of different transformers. We present a new tool, AP+ Verifier, based upon a new algorithm for computing atomic predicates for networks with both packet filters and transformers. For performance evaluation, we use network datasets with different types of transformers (i.e., MPLS tunnels, IP-in-IP tunnels, and NATs). We found that AP+ Verifier is more time and space efficient than prior tools by orders of magnitude.
The Internet consists a large collection of networks. To debug reachability problems, a network operator often asks operators of other networks for help by telephone or email. We present a new protocol, COVE, and an efficient data structure for automating the exchange of data plane reachability information between networks in a business relationship. COVE is designed to improve a network's views of forward and reverse reachability with partial deployment in mind. COVE is scalable to very large networks in the Internet. We illustrate applications of COVE to perform useful network management tasks, which cannot be done effectively using existing
methods and tools.
Advisors/Committee Members: Lam, Simon S., 1947- (advisor), Emerson, Ernest A. (committee member), Garg, Vijay K. (committee member), Gouda, Mohamed G. (committee member), Mok, Aloysius K. (committee member).
Subjects/Keywords: Network verification; Formal methods; Automated tools
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Yang, H. (2015). Efficient verification of packet networks. (Doctoral Dissertation). University of Texas – Austin. Retrieved from http://hdl.handle.net/2152/33271
Chicago Manual of Style (16th Edition):
Yang, Hongkun. “Efficient verification of packet networks.” 2015. Doctoral Dissertation, University of Texas – Austin. Accessed January 18, 2021.
http://hdl.handle.net/2152/33271.
MLA Handbook (7th Edition):
Yang, Hongkun. “Efficient verification of packet networks.” 2015. Web. 18 Jan 2021.
Vancouver:
Yang H. Efficient verification of packet networks. [Internet] [Doctoral dissertation]. University of Texas – Austin; 2015. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/2152/33271.
Council of Science Editors:
Yang H. Efficient verification of packet networks. [Doctoral Dissertation]. University of Texas – Austin; 2015. Available from: http://hdl.handle.net/2152/33271
The Ohio State University
13.
Zaccai, Diego Sebastian.
A Balanced Verification Effort for the Java Language.
Degree: PhD, Computer Science and Engineering, 2016, The Ohio State University
URL: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
► Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing…
(more)
▼ Current tools used to verify software in languages
with reference semantics, such as Java, are hampered by the
possibility of aliases. Existing approaches to addressing this
long-standing verification problem try not to sacrifice modularity
because modular reasoning is what makes verification tractable. To
achieve this, these approaches treat the value of a reference
variable as a memory address in the heap. A serious problem with
this decision is that it severely limits the usefulness of generic
collections because they must be specified as collections of
references, and components of this kind are fundamentally flawed in
design and implementation. The limitations become clear when
attempting to verify clients of generic collections.The first step
in rectifying the situation is to redefine the "value" of a
reference variable in terms of the abstract value of the object it
references. A careful analysis of what the "value" of a reference
variable might mean leads inevitably to this conclusion, which is
consistent with the denotation of a variable in languages with
value semantics, such as RESOLVE. Verification in languages with
value semantics is straightforward compared to verification in
languages with reference semantics precisely because of the lack of
concern with heap properties. However, there is still a nagging
problem: aliasing can occur in legal programs in languages with
reference semantics, such as Java, and it must be handled when it
does occur. The crux of the issue is not in-your-face assignment
statements that copy references but rather aliasing arising within
(hidden) method bodies. The reason is that the effects of calls to
these
methods in client code must be summarized in their
specifications in order to preserve modularity.So, the second step
is the introduction of a discipline restricting what a client can
do with a reference that is aliased within a method. The discipline
advertises the creation of such aliases in method specifications
and prevents a client from engaging in behavior that would break
the abstractions of the objects being referenced, as this would
also prevent modular verification. These restrictions allow code to
be specified in terms of the abstract values of objects instead of
treating the values of references as memory addresses in the heap.
Even though the discipline prevents some programming idioms, it
remains flexible enough to allow for most common programs,
including the use of iterators, without the need for workarounds.A
tool can verify that a program satisfies the provisions of this
discipline. Further, it can generate verification conditions that
rely only on abstract object values to demonstrate a program's
correctness. These verification conditions can be discharged by the
theorem-proving tools currently used to verify RESOLVE
programs.
Advisors/Committee Members: Weide, Bruce W. (Advisor).
Subjects/Keywords: Computer Science; Formal Methods; Software Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zaccai, D. S. (2016). A Balanced Verification Effort for the Java Language. (Doctoral Dissertation). The Ohio State University. Retrieved from http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
Chicago Manual of Style (16th Edition):
Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Doctoral Dissertation, The Ohio State University. Accessed January 18, 2021.
http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.
MLA Handbook (7th Edition):
Zaccai, Diego Sebastian. “A Balanced Verification Effort for the Java Language.” 2016. Web. 18 Jan 2021.
Vancouver:
Zaccai DS. A Balanced Verification Effort for the Java Language. [Internet] [Doctoral dissertation]. The Ohio State University; 2016. [cited 2021 Jan 18].
Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.
Council of Science Editors:
Zaccai DS. A Balanced Verification Effort for the Java Language. [Doctoral Dissertation]. The Ohio State University; 2016. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619
University of Oklahoma
14.
Ralston, Ryan.
Translating Clojure to ACL2 for Verification.
Degree: PhD, 2016, University of Oklahoma
URL: http://hdl.handle.net/11244/42982
► Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects. Formal methods, including…
(more)
▼ Software spends a significant portion of its life-cycle in the maintenance phase and over 20% of the maintenance effort is fixing defects.
Formal methods, including verification, can reduce the number of defects in software and lower corrective maintenance, but their industrial adoption has been underwhelming. A significant barrier to adoption is the overhead of converting imperative programming languages, which are common in industry, into the declarative programming languages that are used by
formal methods tools. In comparison, the verification of software written in declarative programming languages is much easier because the conversion into a
formal methods tool is easier. The growing popularity of declarative programming – evident from the rise of multi-paradigm languages such as Javascript, Ruby, and Scala – affords us the opportunity to verify the correctness of software more easily.
Clojure is a declarative language released in 2007 that compiles to bytecode that executes on the Java Virtual Machine (JVM). Despite being a newer, declarative programming language, several companies have already used it to develop commercial products. Clojure shares a Lisp syntax with ACL2, an interactive theorem prover that is used to verify the correctness of software. Since both languages are based on Lisp, code written in either Clojure or ACL2 is easily converted to the other. Therefore, Clojure can conceivably be verified by ACL2 with limited overhead assuming that the underlying behavior of Clojure code matches that of ACL2. ACL2 has been previously used to reason about Java programs through the use of
formal models of the JVM. Since Clojure compiles to JVM bytecode, a similar approach is taken in this dissertation to verify the underlying implementation of Clojure.
The research presented in this dissertation advances techniques to verify Clojure code in ACL2. Clojure and ACL2 are declarative, but they are specifically functional programming languages so the research focuses on two important concepts in functional programming and verification: arbitrary-precision numbers ("bignums") and lists. For bignums, the correctness of a model of addition is verified that addresses issues that arise from the unique representation of bignums in Clojure. Lists, in Clojure, are implemented as a type of sequence. This dissertation demonstrates an abstraction that equates Clojure sequences to ACL2 lists. In support of the research, an existing ACL2 model of the JVM is modified to address specific aspects of compiled Clojure code and the new model is used to verify the correctness of core Clojure functions with respect to corresponding ACL2 functions. The results support the ideas that ACL2 can be used to reason about Clojure code and that
formal methods can be integrated more easily in industrial software development when the implementation corresponds semantically to the verification model.
Advisors/Committee Members: Page, Rex (advisor), Hougen, Dean (advisor), Miller, David (committee member), Jensen, Matthew (committee member), Weaver, Christopher (committee member).
Subjects/Keywords: Software Verification; Formal Methods; Theorem Proving
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ralston, R. (2016). Translating Clojure to ACL2 for Verification. (Doctoral Dissertation). University of Oklahoma. Retrieved from http://hdl.handle.net/11244/42982
Chicago Manual of Style (16th Edition):
Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Doctoral Dissertation, University of Oklahoma. Accessed January 18, 2021.
http://hdl.handle.net/11244/42982.
MLA Handbook (7th Edition):
Ralston, Ryan. “Translating Clojure to ACL2 for Verification.” 2016. Web. 18 Jan 2021.
Vancouver:
Ralston R. Translating Clojure to ACL2 for Verification. [Internet] [Doctoral dissertation]. University of Oklahoma; 2016. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/11244/42982.
Council of Science Editors:
Ralston R. Translating Clojure to ACL2 for Verification. [Doctoral Dissertation]. University of Oklahoma; 2016. Available from: http://hdl.handle.net/11244/42982
Université de Grenoble
15.
Qamar, Muhammad Nafees.
Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z.
Degree: Docteur es, Informatique, 2011, Université de Grenoble
URL: http://www.theses.fr/2011GRENM057
► L'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et…
(more)
▼ L'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications.
Specifying security-critical software urges to develop techniques that allow early bugs detection and prevention. This is aggravated by the fact that massive cost and time are spent during product validation and verification (V&V). There exists a multitude of formal and informal techniques striving to confront the challenge of specifying and validating specifications. Our approach mainly concerns…
Advisors/Committee Members: Ledru, Yves (thesis director), Idani, Akram (thesis director).
Subjects/Keywords: Information systems; Formal methods; Z; UML; Information systems; Formal methods; Z; UML; 004
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Qamar, M. N. (2011). Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z. (Doctoral Dissertation). Université de Grenoble. Retrieved from http://www.theses.fr/2011GRENM057
Chicago Manual of Style (16th Edition):
Qamar, Muhammad Nafees. “Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z.” 2011. Doctoral Dissertation, Université de Grenoble. Accessed January 18, 2021.
http://www.theses.fr/2011GRENM057.
MLA Handbook (7th Edition):
Qamar, Muhammad Nafees. “Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z.” 2011. Web. 18 Jan 2021.
Vancouver:
Qamar MN. Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z. [Internet] [Doctoral dissertation]. Université de Grenoble; 2011. [cited 2021 Jan 18].
Available from: http://www.theses.fr/2011GRENM057.
Council of Science Editors:
Qamar MN. Spécification et animation de modèles de conception de la sécurité avec Z : Specification and animation of security design models using Z. [Doctoral Dissertation]. Université de Grenoble; 2011. Available from: http://www.theses.fr/2011GRENM057
16.
FARIAS, Adalberto Cajueiro de.
Abstraction of infinite and communicating CSPZ processes
.
Degree: 2009, Universidade Federal de Pernambuco
URL: http://repositorio.ufpe.br/handle/123456789/1364
► Esta tese trata de um problema muito comum em verificação formal: explosão de estados. O problema desabilita a verificação automática de propriedades através da verificação…
(more)
▼ Esta tese trata de um problema muito comum em verificação
formal: explosão de estados.
O problema desabilita a verificação automática de propriedades através da verificação de
modelos. Isto é superado pelo uso de abstração de dados, em que o espaço de estados de
umsistema é reduzido usandoumprincípio simples: descartando detalhes de tal forma que
o espaço de estados torna-se finito exibindo ainda propriedades desejáveis. Isso habilita o
uso de verificacao de modelos, já que o modelo mais simples (abstrato) pode ser usado no
lugar do modelo original (concreto). Entretanto, abstrações podem perder propriedades já
que o nível de precisão é degradado, para algumas propriedades.
Abstrair tipos de dados é, normalmente, uma tarefa não-trivial e requer uma profunda
experiência: o usuário deve prover domínios abstratos, uma relacao matemática entre os
estados (concreto e abstrato), uma inicialização abstrata, e uma versão abstrata para cada
operação. A abordagem proposta nesta tese transfere a maior parte dessa experiência para
um procedimento sistemático que calcula relações de abstração. Essas relações são a base
para as relações matemáticas entre os estados, como também suas imagens determinam os
domínios abstratos (os valores de dados mínimos para preservar propriedades). Também
propomos meta-modelos para estabelecer como o sistema abstrato é inicializado e como
operações são tornadas fechadas sob os domínios abstratos. Isso elimina o conhecimento
requerido do usuário para fornecer as versões abstratas para a inicialização e operações. Os
meta-modelos garantem a correspondência entre os sistemas concreto e abstrato. Assim,
nós derivamos especificações abstratasa partir de concretas de tal formaque a especificação
concreta é mais determinística que a abstrata por construção. Esta é a idéia por trás da teoria
sobrejacente de nossa abordagem de abstração de dados: refinamento de dados.
A notação adotada é CSPZ uma integração
formal das linguagens de especificação CSP
e Z. Uma especificação CSPZ tem duas partes: uma parte comportamental (CSP) e outra de
dados (Z). O procedimento de cálculo foca na parte de Z, mas os resultados são usados na
especificação CSPZ por completo; isso segue da independência de dados da parte de CSP (os
dados não podem afetar seu comportamento). Ao final, a verificação automática é obtida
pela conversão da especificação CSPZ em CSP puro e em seguida pelo reuso do verificador
de modelos padrão de CSP.
Nossa abordagem compreende as seguintes tarefas: nós extraímos a parte de Z de uma
especificação CSPZ (puramente sintática), calculamos as relações de abstração (através de
uma análise sistemática de predicados com uso de ferramenta de suporte), construímos as
relações matemáticas entre os estados, os esquemas abstratos (definidos por meta-modelos),
e realizamos um pós-processamento na especificação abstrata. A última tarefa pode resultar
em alguns ajustes nas relações de abstração. A novidade prática e maior contribuição de
nossa abordagem é o cálculo sistemático das…
Advisors/Committee Members: MOTA, Alexandre Cabral (advisor).
Subjects/Keywords: Formal methods;
Formal specification;
CSPZ;
Data abstraction;
Data refinement,
Process refinement;
Model checking
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
FARIAS, A. C. d. (2009). Abstraction of infinite and communicating CSPZ processes
. (Thesis). Universidade Federal de Pernambuco. Retrieved from http://repositorio.ufpe.br/handle/123456789/1364
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
FARIAS, Adalberto Cajueiro de. “Abstraction of infinite and communicating CSPZ processes
.” 2009. Thesis, Universidade Federal de Pernambuco. Accessed January 18, 2021.
http://repositorio.ufpe.br/handle/123456789/1364.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
FARIAS, Adalberto Cajueiro de. “Abstraction of infinite and communicating CSPZ processes
.” 2009. Web. 18 Jan 2021.
Vancouver:
FARIAS ACd. Abstraction of infinite and communicating CSPZ processes
. [Internet] [Thesis]. Universidade Federal de Pernambuco; 2009. [cited 2021 Jan 18].
Available from: http://repositorio.ufpe.br/handle/123456789/1364.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
FARIAS ACd. Abstraction of infinite and communicating CSPZ processes
. [Thesis]. Universidade Federal de Pernambuco; 2009. Available from: http://repositorio.ufpe.br/handle/123456789/1364
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Universitat Politècnica de València
17.
Peiró Frasquet, Salvador.
Metodología para hipervisores seguros utilizando técnicas de validación formal
.
Degree: 2016, Universitat Politècnica de València
URL: http://hdl.handle.net/10251/63152
► [EN] The availability of new processors with more processing power for embedded systems has raised the development of applications that tackle problems of greater complexity.…
(more)
▼ [EN] The availability of new processors with more processing power for embedded systems has raised
the development of applications that tackle problems of greater complexity. Currently, the
embedded applications have more features, and as a consequence, more complexity. For this
reason, there exists a growing interest in allowing the secure execution of multiple applications
that share a single processor and memory. In this context, partitioned system architectures based
on hypervisors have evolved as an adequate solution to build secure systems.
One of the main challenges in the construction of secure partitioned systems is the verification of
the correct operation of the hypervisor, since, the hypervisor is the critical component on which
rests the security of the partitioned system. Traditional approaches for Validation and Verification
(V&V), such as testing, inspection and analysis, present limitations for the exhaustive validation
and verification of the system operation, due to the fact that the input space to validate grows
exponentially with respect to the number of inputs to validate. Given this limitations, verification
techniques based in
formal methods arise as an alternative to complement the traditional validation
techniques.
This dissertation focuses on the application of
formal methods to validate the correctness of the
partitioned system, with a special focus on the XtratuM hypervisor. The proposed methodology
is evaluated through its application to the hypervisor validation. To this end, we propose a
formal
model of the hypervisor based in Finite State Machines (FSM), this model enables the definition
of the correctness properties that the hypervisor design must fulfill. In addition, this dissertation
studies how to ensure the functional correctness of the hypervisor implementation by means of
deductive code verification techniques.
Last, we study the vulnerabilities that result of the loss of confidentiality (CWE-200 [CWE08b]) of
the information managed by the partitioned system. In this context, the vulnerabilities (infoleaks)
are modeled, static code analysis techniques are applied to the detection of the vulnerabilities,
and last the proposed techniques are validated by means of a practical case study on the Linux
kernel that is a component of the partitioned system.; [ES] La disponibilidad de nuevos procesadores más potentes para aplicaciones empotradas ha permitido
el desarrollo de aplicaciones que abordan problemas de mayor complejidad. Debido a esto, las
aplicaciones empotradas actualmente tienen más funciones y prestaciones, y como consecuencia de
esto, una mayor complejidad. Por este motivo, existe un interés creciente en permitir la ejecución
de múltiples aplicaciones de forma segura y sin interferencias en un mismo procesador y memoria.
En este marco surgen las arquitecturas de sistemas particionados basados en hipervisores como
una solución apropiada para construir sistemas seguros.
Uno de los principales retos en la construcción de sistemas particionados, es la verificación del…
Advisors/Committee Members: Crespo Lorente, Alfons (advisor), Masmano Tello, Miguel Ángel (advisor), Simó Ten, José Enrique (advisor).
Subjects/Keywords: Secure Hypervisor construction using formal verification;
Partitioned system;
Hypervisor;
Formal methods;
Security;
Validation and verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Peiró Frasquet, S. (2016). Metodología para hipervisores seguros utilizando técnicas de validación formal
. (Doctoral Dissertation). Universitat Politècnica de València. Retrieved from http://hdl.handle.net/10251/63152
Chicago Manual of Style (16th Edition):
Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal
.” 2016. Doctoral Dissertation, Universitat Politècnica de València. Accessed January 18, 2021.
http://hdl.handle.net/10251/63152.
MLA Handbook (7th Edition):
Peiró Frasquet, Salvador. “Metodología para hipervisores seguros utilizando técnicas de validación formal
.” 2016. Web. 18 Jan 2021.
Vancouver:
Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal
. [Internet] [Doctoral dissertation]. Universitat Politècnica de València; 2016. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10251/63152.
Council of Science Editors:
Peiró Frasquet S. Metodología para hipervisores seguros utilizando técnicas de validación formal
. [Doctoral Dissertation]. Universitat Politècnica de València; 2016. Available from: http://hdl.handle.net/10251/63152
18.
Hjort, Rikard.
Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
.
Degree: Chalmers tekniska högskola / Institutionen för data och informationsteknik, 2020, Chalmers University of Technology
URL: http://hdl.handle.net/20.500.12380/300761
► A smart contract is immutable, public bytecode which handles valuable assets. This makes it a prime target for formal methods. WebAssembly (Wasm) is emerging as…
(more)
▼ A smart contract is immutable, public bytecode which handles valuable assets. This
makes it a prime target for formal methods. WebAssembly (Wasm) is emerging
as bytecode format for smart contracts. KWasm is a prototype mechanization of
Wasm in the K framework which can be used for formal verification. The current
project aims to verify a single Wasm smart contract, a simple token contract. First,
we complete the KWasm semantics to be able to deal with modules and test the
semantics against the official conformance tests. This reveals several shortcomings
of the conformance tests. Second, we create an Ethereum embedding by creating
a separate Ethereum client semantics and combining it with the KWasm semantics
through a thin, synchronizing interface. This embedding is then unit tested,
including conformance tests for two variants of the WRC20 contracts. Thirdly, we
use the KWasm semantics to prove properties of incrementally more complex Wasm
programs, with an emphasis on heap reasoning, culminating in the verification of a
helper function that reverses the bytes of a 64-bit integer. In the process we add
25 axioms that get upstreamed into K, and several more that are useful for general
Wasm verification.
Subjects/Keywords: K;
K framework;
WebAssembly;
Wasm;
Ethereum;
Ewasm;
formal methods;
formal verification;
semantics;
specification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Hjort, R. (2020). Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
. (Thesis). Chalmers University of Technology. Retrieved from http://hdl.handle.net/20.500.12380/300761
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Hjort, Rikard. “Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
.” 2020. Thesis, Chalmers University of Technology. Accessed January 18, 2021.
http://hdl.handle.net/20.500.12380/300761.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Hjort, Rikard. “Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
.” 2020. Web. 18 Jan 2021.
Vancouver:
Hjort R. Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
. [Internet] [Thesis]. Chalmers University of Technology; 2020. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/20.500.12380/300761.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Hjort R. Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
. [Thesis]. Chalmers University of Technology; 2020. Available from: http://hdl.handle.net/20.500.12380/300761
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
19.
Bockenek, Joshua A.
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.
Degree: MS, Computer Engineering, 2017, Virginia Tech
URL: http://hdl.handle.net/10919/81710
► Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such…
(more)
▼ Writing bug-free code is fraught with difficulty, and existing tools for the
formal verification of programs do not scale well to large, complicated codebases such as that of systems software (OSes, compilers, and similar programs that have a high level of complexity but work on a lower level than typical user applications such as text editors, image viewers, and the like). This thesis presents USIMPL, a component of the Orca project for
formal verification that builds on an existing framework for computer-aided, deductive mathematical proofs (Foster’s Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmer’s Simpl) in order to achieve a modular, scalable framework for proofs of program correctness utilizing the rule-based mathematical representation of program behavior known as Hoare logic and Hoare-style algebraic laws of programming, which provide a
formal methodology for transforming programs to equivalent formulations.
Advisors/Committee Members: Ravindran, Binoy (committeechair), Lammich, Peter (committee member), Broadwater, Robert P. (committee member).
Subjects/Keywords: Formal Verification; Formal Methods; Isabelle; Unifying Theories of Programming; Verification Condition Generation
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Bockenek, J. A. (2017). USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. (Masters Thesis). Virginia Tech. Retrieved from http://hdl.handle.net/10919/81710
Chicago Manual of Style (16th Edition):
Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Masters Thesis, Virginia Tech. Accessed January 18, 2021.
http://hdl.handle.net/10919/81710.
MLA Handbook (7th Edition):
Bockenek, Joshua A. “USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow.” 2017. Web. 18 Jan 2021.
Vancouver:
Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Internet] [Masters thesis]. Virginia Tech; 2017. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10919/81710.
Council of Science Editors:
Bockenek JA. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow. [Masters Thesis]. Virginia Tech; 2017. Available from: http://hdl.handle.net/10919/81710
Universidade do Rio Grande do Norte
20.
Souza, Diego Henrique Oliveira de.
Joker: um realizador de desenhos animados para linguagens formais
.
Degree: 2011, Universidade do Rio Grande do Norte
URL: http://repositorio.ufrn.br/handle/123456789/18024
► Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However,…
(more)
▼ Using
formal methods, the developer can increase software s trustiness and correctness.
Furthermore, the developer can concentrate in the functional requirements of the
software. However, there are many resistance in adopting this software development
approach. The main reason is the scarcity of adequate, easy to use, and useful tools.
Developers typically write code and test it. These tests usually consist of executing the
program and checking its output against its requirements. This, however, is not always
an exhaustive discipline. On the other side, using
formal methods one might be able
to investigate the system s properties further. Unfortunately, specification languages do
not always have tools like animators or simulators, and sometimes there are no friendly
Graphical User Interfaces. On the other hand, specification languages usually have a compiler
which normally generates a Labeled Transition System (LTS). This work proposes
an application that provides graphical animation for
formal specifications using the LTS
as input. The application initially supports the languages B, CSP, and Z. However, using a
LTS in a specified XML format, it is possible to animate further languages. Additionally,
the tool provides traces visualization, the choices the user did, in a graphical tree. The
intention is to improve the comprehension of a specification by providing information
about errors and animating it, as the developers do for programming languages, such as
Java and C++.
Advisors/Committee Members: Oliveira, Marcel Vinicius Medeiros (advisor), CPF:02386943488 (advisor), http://lattes.cnpq.br/1756952696097255 (advisor).
Subjects/Keywords: Interface Gráfica;
Animação;
Java;
Especificação formal;
Métodos formais.;
Graphical User Interface;
Animation;
Java;
Formal Specifications;
Formal Methods.
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Souza, D. H. O. d. (2011). Joker: um realizador de desenhos animados para linguagens formais
. (Thesis). Universidade do Rio Grande do Norte. Retrieved from http://repositorio.ufrn.br/handle/123456789/18024
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais
.” 2011. Thesis, Universidade do Rio Grande do Norte. Accessed January 18, 2021.
http://repositorio.ufrn.br/handle/123456789/18024.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais
.” 2011. Web. 18 Jan 2021.
Vancouver:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais
. [Internet] [Thesis]. Universidade do Rio Grande do Norte; 2011. [cited 2021 Jan 18].
Available from: http://repositorio.ufrn.br/handle/123456789/18024.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais
. [Thesis]. Universidade do Rio Grande do Norte; 2011. Available from: http://repositorio.ufrn.br/handle/123456789/18024
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
21.
Diego Henrique Oliveira de Souza.
Joker: um realizador de desenhos animados para linguagens formais.
Degree: 2011, Universidade Federal do Rio Grande do Norte
URL: http://bdtd.bczm.ufrn.br/tedesimplificado//tde_busca/arquivo.php?codArquivo=4515
► Usando métodos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Além disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Porém há…
(more)
▼ Usando métodos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Além disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Porém há muita resistência em se adotar essa abordagem de desenvolvimento de software. A razão principal e a escassez de suporte ferramental adequado, útil e de fácil utilização. Os desenvolvedores normalmente escrevem o código e o testam. Estes testes geralmente consistem em checar se as saídas estão de acordo com os requisitos. Isto, contudo, nem sempre e possível de maneira exaustiva. Por outro lado, usando Métodos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especificação formal nem sempre possuem ferramentas como animador ou simulador e às vezes não há interfaces gráficas amigáveis. Porém, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transições Rotuladas (LTS). A proposta deste trabalho é desenvolver um aplicativo que fornece animação gráfica para especificações formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado é possível animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualização de traces, escolhas feitas pelo usuário, em um formato de árvore gráfica. A intenção é melhorar a compreensão de uma especificação, fornecendo informações sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programação como Java e C++.
Using formal methods, the developer can increase softwares trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the systems properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.
Advisors/Committee Members: Alexandre Cabral Mota, Jair Cavalcanti Leite, Marcel Vinicius Medeiros Oliveira.
Subjects/Keywords: Interface Gráfica; Animação; Java; Especificação formal; Métodos formais.; SISTEMAS DE COMPUTACAO; Graphical User Interface; Animation; Java; Formal Specifications; Formal Methods.
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Souza, D. H. O. d. (2011). Joker: um realizador de desenhos animados para linguagens formais. (Thesis). Universidade Federal do Rio Grande do Norte. Retrieved from http://bdtd.bczm.ufrn.br/tedesimplificado//tde_busca/arquivo.php?codArquivo=4515
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais.” 2011. Thesis, Universidade Federal do Rio Grande do Norte. Accessed January 18, 2021.
http://bdtd.bczm.ufrn.br/tedesimplificado//tde_busca/arquivo.php?codArquivo=4515.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais.” 2011. Web. 18 Jan 2021.
Vancouver:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais. [Internet] [Thesis]. Universidade Federal do Rio Grande do Norte; 2011. [cited 2021 Jan 18].
Available from: http://bdtd.bczm.ufrn.br/tedesimplificado//tde_busca/arquivo.php?codArquivo=4515.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais. [Thesis]. Universidade Federal do Rio Grande do Norte; 2011. Available from: http://bdtd.bczm.ufrn.br/tedesimplificado//tde_busca/arquivo.php?codArquivo=4515
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Universidade do Rio Grande do Norte
22.
Souza, Diego Henrique Oliveira de.
Joker: um realizador de desenhos animados para linguagens formais
.
Degree: 2011, Universidade do Rio Grande do Norte
URL: http://repositorio.ufrn.br/handle/123456789/18024
► Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However,…
(more)
▼ Using
formal methods, the developer can increase software s trustiness and correctness.
Furthermore, the developer can concentrate in the functional requirements of the
software. However, there are many resistance in adopting this software development
approach. The main reason is the scarcity of adequate, easy to use, and useful tools.
Developers typically write code and test it. These tests usually consist of executing the
program and checking its output against its requirements. This, however, is not always
an exhaustive discipline. On the other side, using
formal methods one might be able
to investigate the system s properties further. Unfortunately, specification languages do
not always have tools like animators or simulators, and sometimes there are no friendly
Graphical User Interfaces. On the other hand, specification languages usually have a compiler
which normally generates a Labeled Transition System (LTS). This work proposes
an application that provides graphical animation for
formal specifications using the LTS
as input. The application initially supports the languages B, CSP, and Z. However, using a
LTS in a specified XML format, it is possible to animate further languages. Additionally,
the tool provides traces visualization, the choices the user did, in a graphical tree. The
intention is to improve the comprehension of a specification by providing information
about errors and animating it, as the developers do for programming languages, such as
Java and C++.
Advisors/Committee Members: Oliveira, Marcel Vinicius Medeiros (advisor), CPF:02386943488 (advisor), http://lattes.cnpq.br/1756952696097255 (advisor).
Subjects/Keywords: Interface Gráfica;
Animação;
Java;
Especificação formal;
Métodos formais.;
Graphical User Interface;
Animation;
Java;
Formal Specifications;
Formal Methods.
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Souza, D. H. O. d. (2011). Joker: um realizador de desenhos animados para linguagens formais
. (Masters Thesis). Universidade do Rio Grande do Norte. Retrieved from http://repositorio.ufrn.br/handle/123456789/18024
Chicago Manual of Style (16th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais
.” 2011. Masters Thesis, Universidade do Rio Grande do Norte. Accessed January 18, 2021.
http://repositorio.ufrn.br/handle/123456789/18024.
MLA Handbook (7th Edition):
Souza, Diego Henrique Oliveira de. “Joker: um realizador de desenhos animados para linguagens formais
.” 2011. Web. 18 Jan 2021.
Vancouver:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais
. [Internet] [Masters thesis]. Universidade do Rio Grande do Norte; 2011. [cited 2021 Jan 18].
Available from: http://repositorio.ufrn.br/handle/123456789/18024.
Council of Science Editors:
Souza DHOd. Joker: um realizador de desenhos animados para linguagens formais
. [Masters Thesis]. Universidade do Rio Grande do Norte; 2011. Available from: http://repositorio.ufrn.br/handle/123456789/18024
Virginia Tech
23.
Moustafa, Iman Saleh.
Formal Specification and Verification of Data-Centric Web Services.
Degree: PhD, Computer Science, 2012, Virginia Tech
URL: http://hdl.handle.net/10919/26294
► In this thesis, we develop and evaluate a formal model and contracting framework for data-centric Web services. The central component of our framework is a…
(more)
▼ In this thesis, we develop and evaluate a
formal model and contracting framework for data-centric Web services. The central component of our framework is a
formal specification of a common Create-Read-Update-Delete (CRUD) data store. We show how this model can be used in the
formal specification and verification of both basic and transactional Web service compositions. We demonstrate through both
formal proofs and empirical evaluations that our proposed framework significantly decreases ambiguity about a service, enhances its reuse, and facilitates detection of errors in service-based implementations.
Web Services are reusable software components that make use of standardized interfaces to enable loosely-coupled business-to-business and customer-to-business interactions over the Web. In such environments, service consumers depend heavily on the service interface specification to discover, invoke, and synthesize services over the Web. Data-centric Web services are services whose behavior is determined by their interactions with a repository of stored data. A major challenge in this domain is interpreting the data that must be marshaled between consumer and producer systems. While the Web Services Description Language (WSDL) is currently the de facto standard for Web services, it only specifies a service operation in terms of its syntactical inputs and outputs; it does not provide a means for specifying the underlying data model, nor does it specify how a service invocation affects the data. The lack of data specification potentially leads to erroneous use of the service by a consumer. In this work, we propose a
formal contract for data-centric Web services. The goal is to formally and unambiguously specify the service behavior in terms of its underlying data model and data interactions. We address the specification of a single service, a flow of services interacting with a single data store, and also the specification of distributed transactions involving multiple Web services interacting with different autonomous data stores. We use the proposed
formal contract to decrease ambiguity about a service behavior, to fully verify a composition of services, and to guarantee correctness and data integrity properties within a transactional composition of services.
Advisors/Committee Members: Kulczycki, Gregory W. (committeechair), Kulczycki, Gregory W. (committeechair), Chen, Ing-Ray (committee member), Egyhazy, Csaba J. (committee member), Frakes, William B. (committee member), Chen, Ing-Ray (committee member), Egyhazy, Csaba J. (committee member), Frakes, William B. (committee member), Blake, M. Brian (committeecochair), Blake, M. Brian (committeecochair).
Subjects/Keywords: Formal Methods; Data Modeling; Software Specification and Verification; Formal Methods; Data Modeling; Software Specification and Verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Moustafa, I. S. (2012). Formal Specification and Verification of Data-Centric Web Services. (Doctoral Dissertation). Virginia Tech. Retrieved from http://hdl.handle.net/10919/26294
Chicago Manual of Style (16th Edition):
Moustafa, Iman Saleh. “Formal Specification and Verification of Data-Centric Web Services.” 2012. Doctoral Dissertation, Virginia Tech. Accessed January 18, 2021.
http://hdl.handle.net/10919/26294.
MLA Handbook (7th Edition):
Moustafa, Iman Saleh. “Formal Specification and Verification of Data-Centric Web Services.” 2012. Web. 18 Jan 2021.
Vancouver:
Moustafa IS. Formal Specification and Verification of Data-Centric Web Services. [Internet] [Doctoral dissertation]. Virginia Tech; 2012. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10919/26294.
Council of Science Editors:
Moustafa IS. Formal Specification and Verification of Data-Centric Web Services. [Doctoral Dissertation]. Virginia Tech; 2012. Available from: http://hdl.handle.net/10919/26294
Carnegie Mellon University
24.
Tschantz, Michael Carl.
Formalizing and Enforcing Purpose Restrictions.
Degree: 2012, Carnegie Mellon University
URL: http://repository.cmu.edu/dissertations/128
► Privacy policies often place restrictions on the purposes for which a governed entity may use personal information. For example, regulations, such as the Health Insurance…
(more)
▼ Privacy policies often place restrictions on the purposes for which a governed entity may use personal information. For example, regulations, such as the Health Insurance Portability and Accountability Act (HIPAA), require that hospital employees use medical information for only certain purposes, such as treatment, but not for others, such as gossip. Thus, using formal or automated methods for enforcing privacy policies requires a semantics of purpose restrictions to determine whether an action is for a purpose. We provide such a semantics using a formalism based on planning. We model planning using a modified version of Markov Decision Processes (MDPs), which exclude redundant actions for a formal definition of redundant. We argue that an action is for a purpose if and only if the action is part of a plan for optimizing the satisfaction of that purpose under the MDP model. We use this formalization to define when a sequence of actions is only for or not for a purpose. This semantics enables us to create and implement an algorithm for automating auditing, and to describe formally and compare rigorously previous enforcement methods. We extend this formalization to Partially Observable Markov Decision Processes (POMDPs) to answer when information is used for a purpose. To validate our semantics, we provide an example application and conduct a survey to compare our semantics to how people commonly understand the word “purpose”.
Subjects/Keywords: Privacy; Formal Methods; Auditing; Compliance Checking; Planning; MDPs; POMDPs; Computer Sciences
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Tschantz, M. C. (2012). Formalizing and Enforcing Purpose Restrictions. (Thesis). Carnegie Mellon University. Retrieved from http://repository.cmu.edu/dissertations/128
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Tschantz, Michael Carl. “Formalizing and Enforcing Purpose Restrictions.” 2012. Thesis, Carnegie Mellon University. Accessed January 18, 2021.
http://repository.cmu.edu/dissertations/128.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Tschantz, Michael Carl. “Formalizing and Enforcing Purpose Restrictions.” 2012. Web. 18 Jan 2021.
Vancouver:
Tschantz MC. Formalizing and Enforcing Purpose Restrictions. [Internet] [Thesis]. Carnegie Mellon University; 2012. [cited 2021 Jan 18].
Available from: http://repository.cmu.edu/dissertations/128.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Tschantz MC. Formalizing and Enforcing Purpose Restrictions. [Thesis]. Carnegie Mellon University; 2012. Available from: http://repository.cmu.edu/dissertations/128
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of California – Berkeley
25.
Sadigh, Dorsa.
Safe and Interactive Autonomy: Control, Learning, and Verification.
Degree: Electrical Engineering & Computer Sciences, 2017, University of California – Berkeley
URL: http://www.escholarship.org/uc/item/06g4b5xs
► The goal of my research is to enable safe and reliable integration of human-robot systems in our society by providing a unified framework for modeling…
(more)
▼ The goal of my research is to enable safe and reliable integration of human-robot systems in our society by providing a unified framework for modeling and design of these systems. Today's society is rapidly advancing towards autonomous systems that interact and collaborate with humans, e.g., semiautonomous vehicles interacting with drivers and pedestrians, medical robots used in collaboration with doctors, or service robots interacting with their users in smart homes. The safety-critical nature of these systems require us to provide provably correct guarantees about their performance. In this dissertation, we develop a formalism for the design of algorithms and mathematical models that enable correct-by-construction control and verification of human-robot systems.We focus on two natural instances of this agenda. In the first part, we study interaction-aware control, where we use algorithmic HRI to be mindful of the effects of autonomous systems on humans' actions, and further leverage these effects for better safety, efficiency, coordination, and estimation. We further use active learning techniques to update and better learn human models, and study the accuracy and robustness of these models. In the second part, we address the problem of providing correctness guarantees, while taking into account the uncertainty arising from the environment or human models. Through this effort, we introduce Probabilistic Signal Temporal Logic (PrSTL), an expressive specification language that allows representing Bayesian graphical models as part of its predicates. Further, we provide a solution for synthesizing controllers that satisfy temporal logic specifications in probabilistic and reactive settings, and discuss a diagnosis and repair algorithm for systematic transfer of control to the human in unrealizable settings.While the algorithms and techniques introduced can be applied to many human-robot systems, in this dissertation, we will mainly focus on the implications of my work for semiautonomous driving.
Subjects/Keywords: Engineering; Control theory; Formal methods; Human-Robot Interaction
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Sadigh, D. (2017). Safe and Interactive Autonomy: Control, Learning, and Verification. (Thesis). University of California – Berkeley. Retrieved from http://www.escholarship.org/uc/item/06g4b5xs
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Sadigh, Dorsa. “Safe and Interactive Autonomy: Control, Learning, and Verification.” 2017. Thesis, University of California – Berkeley. Accessed January 18, 2021.
http://www.escholarship.org/uc/item/06g4b5xs.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Sadigh, Dorsa. “Safe and Interactive Autonomy: Control, Learning, and Verification.” 2017. Web. 18 Jan 2021.
Vancouver:
Sadigh D. Safe and Interactive Autonomy: Control, Learning, and Verification. [Internet] [Thesis]. University of California – Berkeley; 2017. [cited 2021 Jan 18].
Available from: http://www.escholarship.org/uc/item/06g4b5xs.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Sadigh D. Safe and Interactive Autonomy: Control, Learning, and Verification. [Thesis]. University of California – Berkeley; 2017. Available from: http://www.escholarship.org/uc/item/06g4b5xs
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of California – Berkeley
26.
Chen, Zhijie.
Abstract Semantics for Software Security Analysis.
Degree: Computer Science, 2015, University of California – Berkeley
URL: http://www.escholarship.org/uc/item/7bn8t9xb
► Program analysis and formal methods have enabled advanced automatic software security analysis such as security policy enforcement and vulnerability discovery. However, due to the complexity…
(more)
▼ Program analysis and formal methods have enabled advanced automatic software security analysis such as security policy enforcement and vulnerability discovery. However, due to the complexity of the modern software, recent applications of such techniques exhibit serious usability and scalability problems. In this thesis, we address these problems usingautomatically or semi-automatically constructed abstract program semantics. Specifically, we study two typical scenarios where the power of formal techniques is limited by the problems above, and develop novel techniques that address these issues. First, we propose a newalgorithm to construct event-based program abstraction, and check contextual security policies under this abstraction. Our approach addresses the usability and scalability problems in the model-checking of security policies in event-driven programs. Second, we propose a synthesis-based algorithm to learn and check web server logic without having access to theserver-side source code. The key insight is that the client-side behavior reflects partially the server-side logic, thus we infer server-side logic by observing the client-side’s execution. We develop a declarative language to encode our domain specific modeling of common server-side operations, as well as an efficient algorithm to synthesize a server model in that language. In summary, we demonstrate that abstract semantics can bridge the gap between the human and the massive details of the program, and make formal techniques applicable in a large scale.
Subjects/Keywords: Computer science; Formal Methods; Mobile; Program Analysis; Security; Software; Web
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Chen, Z. (2015). Abstract Semantics for Software Security Analysis. (Thesis). University of California – Berkeley. Retrieved from http://www.escholarship.org/uc/item/7bn8t9xb
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Chen, Zhijie. “Abstract Semantics for Software Security Analysis.” 2015. Thesis, University of California – Berkeley. Accessed January 18, 2021.
http://www.escholarship.org/uc/item/7bn8t9xb.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Chen, Zhijie. “Abstract Semantics for Software Security Analysis.” 2015. Web. 18 Jan 2021.
Vancouver:
Chen Z. Abstract Semantics for Software Security Analysis. [Internet] [Thesis]. University of California – Berkeley; 2015. [cited 2021 Jan 18].
Available from: http://www.escholarship.org/uc/item/7bn8t9xb.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Chen Z. Abstract Semantics for Software Security Analysis. [Thesis]. University of California – Berkeley; 2015. Available from: http://www.escholarship.org/uc/item/7bn8t9xb
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Alberta
27.
Delfani, Parisa.
Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors.
Degree: MS, Department of Computing Science, 2012, University of Alberta
URL: https://era.library.ualberta.ca/files/t722hb17m
► Inexpensive yet versatile limited-capability processors enable computing to be embedded in many kinds of devices and situations. Most applications are simple purpose-programmed reactive systems that…
(more)
▼ Inexpensive yet versatile limited-capability
processors enable computing to be embedded in many kinds of devices
and situations. Most applications are simple purpose-programmed
reactive systems that interact with the environment through sensors
and actuators. Because the processors are limited state-machines,
and in principle can be fully specified, they are amenable to
rigorous formal verification. Low cost wired and wireless
connection schemes permit the easy aggregation of these processors
into networks with both static and dynamic topologies. The
resulting networks will often have unexpected behavior or emergent
properties. This thesis is a step towards formally reasoning about
such networks. Our contribution is a simple domain-specific
programming environment that generates both the model for
performing verification via model checking, and extracts executable
code that runs on the Arduino computing platform.
Subjects/Keywords: Software Engineering; Model Checking; Sensor Networks; Formal Methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Delfani, P. (2012). Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors. (Masters Thesis). University of Alberta. Retrieved from https://era.library.ualberta.ca/files/t722hb17m
Chicago Manual of Style (16th Edition):
Delfani, Parisa. “Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors.” 2012. Masters Thesis, University of Alberta. Accessed January 18, 2021.
https://era.library.ualberta.ca/files/t722hb17m.
MLA Handbook (7th Edition):
Delfani, Parisa. “Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors.” 2012. Web. 18 Jan 2021.
Vancouver:
Delfani P. Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors. [Internet] [Masters thesis]. University of Alberta; 2012. [cited 2021 Jan 18].
Available from: https://era.library.ualberta.ca/files/t722hb17m.
Council of Science Editors:
Delfani P. Behavioral Verification of Small Networks of State-Machines
Built with Arduino-like Processors. [Masters Thesis]. University of Alberta; 2012. Available from: https://era.library.ualberta.ca/files/t722hb17m
28.
Ksystra, Aikaterini.
Enabling reasoning and verification support for intelligent agent systems, using formal methods.
Degree: 2017, National Technical University of Athens (NTUA); Εθνικό Μετσόβιο Πολυτεχνείο (ΕΜΠ)
URL: http://hdl.handle.net/10442/hedi/42255
► Formal methods are techniques, languages and tools based on mathematics, which provide an unambiguous, strict mathematical description or specication which is used for eective design,…
(more)
▼ Formal methods are techniques, languages and tools based on mathematics, which provide an unambiguous, strict mathematical description or specication which is used for eective design, analysis and verication of desired properties of the system. An important branch of formal methods are algebraic specication languages with a rigorous basis on mathematical logical systems or combinations of them. Such a language is CafeOBJ, an executable, new generation algebraic specication language, member of the OBJ family languages. Its main characteristic, that dierentiates it from other formalisms, is its direct support to behavioural specication paradigm since it embeds special hidden sorts and behavioural operators in its syntax. Behavioural specication is based on hidden algebra and supports an object oriented style of algebraic specication. It also supports specication of distributed complex systems as abstract state machines and verication of safety properties of them through theorem proving techniques such as simultaneous induction and coinduction. The scope of the thesis is the modelling and verication of intelligent agents using algebraic specication techniques. By intelligent agents we refer to the systems used in the New or Semantic Web in order to achieve the need for reactivity, interaction and communication between its various components. An intelligent agent can be dened as an autonomous entity which observes through sensors and acts upon an environment using actuators (i.e. it is an agent) and directs its activity towards achieving goals. Due to the special characteristics of such systems, and their increased development as well as their use in critical domains, the requirements for reliability, security and proper functionality has led to the use of formal methods for their analysis and the development of new methodologies oriented to these systems. To this end, in this thesis an algebraic framework is proposed for the specication and verication of two basic types of intelligent systems, those whose behaviour is expressed in terms of reactive rules (reactive rule-based systems) and those who can sense the changes in their physical environment (context-aware systems), and adapt their behaviour accordingly. In the rst category of intelligent agents, we rst give formal semantics, based on the hidden algebra formalism, to the basic reactive rule families, then we formally analyse and verify reactive rule-based systems using equational logic, next we propose the use of rewriting logic for the detection of structural errors of the rules, such as termination and conuence, and nally we compare the proposed approaches. In the second type of agents, which are usually more complex, the specication of the system, is dened as the composition of the specications of3its components, i.e. the specications which describe data types as visible sorts and the various components of the system as Observational Transition Systems, a kind of behavioural object. In this way the complex interactions of such systems can be expressed in a…
Subjects/Keywords: Έξυπνα συστήματα; Τυπικές μέθοδοι; Intelligent agents; Formal methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ksystra, A. (2017). Enabling reasoning and verification support for intelligent agent systems, using formal methods. (Thesis). National Technical University of Athens (NTUA); Εθνικό Μετσόβιο Πολυτεχνείο (ΕΜΠ). Retrieved from http://hdl.handle.net/10442/hedi/42255
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Ksystra, Aikaterini. “Enabling reasoning and verification support for intelligent agent systems, using formal methods.” 2017. Thesis, National Technical University of Athens (NTUA); Εθνικό Μετσόβιο Πολυτεχνείο (ΕΜΠ). Accessed January 18, 2021.
http://hdl.handle.net/10442/hedi/42255.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Ksystra, Aikaterini. “Enabling reasoning and verification support for intelligent agent systems, using formal methods.” 2017. Web. 18 Jan 2021.
Vancouver:
Ksystra A. Enabling reasoning and verification support for intelligent agent systems, using formal methods. [Internet] [Thesis]. National Technical University of Athens (NTUA); Εθνικό Μετσόβιο Πολυτεχνείο (ΕΜΠ); 2017. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/10442/hedi/42255.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Ksystra A. Enabling reasoning and verification support for intelligent agent systems, using formal methods. [Thesis]. National Technical University of Athens (NTUA); Εθνικό Μετσόβιο Πολυτεχνείο (ΕΜΠ); 2017. Available from: http://hdl.handle.net/10442/hedi/42255
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Vanderbilt University
29.
Balasubramanian, Daniel Allen.
Behavioral Semantics of Modeling Languages: A Pragmatic Approach.
Degree: PhD, Computer Science, 2011, Vanderbilt University
URL: http://hdl.handle.net/1803/12061
► Domain-specific modeling languages (DSMLs) are specialized languages tailored with concepts and features of a particular domain. The abstractions offered by DSMLs allow designers of software…
(more)
▼ Domain-specific modeling languages (DSMLs) are specialized languages tailored with concepts and features of a particular domain. The abstractions offered by DSMLs allow designers of software systems to ignore implementation details and instead focus on the system at a high level. While higher levels of abstraction can offer many advantages, there are still unresolved issues with DSMLs. One of these is the difficulty of applying
formal verification
methods.
This dissertation presents two contributions that assist with the
formal verification of domain-specific models. The first is a unified framework in which Statechart models of different semantic variants can be defined, simulated and verified. The key idea is that the user describes only the structure of a model, and then selects the semantics from a set of pluggable components. This allows a single model to be executed using multiple semantics, and a system comprised of interacting models using different semantics can be simulated and verified in a single environment. A lightweight method for specifying properties based on a pattern system was also developed. To perform analysis, the framework is integrated with Java Pathfinder, a software model checker, and Symbolic Pathfinder, its symbolic execution engine. Symbolic execution allows both test-vector generation and reachability analysis.
The second major contribution is an extension to Formula, a modeling language and analysis tool from Microsoft Research, that calculates execution traces of models. The behavioral semantics are defined as a set of model transformations, each of which represents an atomic step of execution. The trace computing extension consists of three components. The first is a component that applies all applicable transformations to an input model at a given step and creates a separate trace for each application. The second component is used to create a separate trace for each non-deterministic choice of the input parameters that are passed to a transformation, making non-determinism inside a single execution step explicit to the trace computing module. The third component stores execution traces efficiently by computing and storing only the differences between consecutive steps in a trace when possible.
Advisors/Committee Members: Gabor Karsai (Committee Chair).
Subjects/Keywords: formal methods; model-based development; Domain-specific languages
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Balasubramanian, D. A. (2011). Behavioral Semantics of Modeling Languages: A Pragmatic Approach. (Doctoral Dissertation). Vanderbilt University. Retrieved from http://hdl.handle.net/1803/12061
Chicago Manual of Style (16th Edition):
Balasubramanian, Daniel Allen. “Behavioral Semantics of Modeling Languages: A Pragmatic Approach.” 2011. Doctoral Dissertation, Vanderbilt University. Accessed January 18, 2021.
http://hdl.handle.net/1803/12061.
MLA Handbook (7th Edition):
Balasubramanian, Daniel Allen. “Behavioral Semantics of Modeling Languages: A Pragmatic Approach.” 2011. Web. 18 Jan 2021.
Vancouver:
Balasubramanian DA. Behavioral Semantics of Modeling Languages: A Pragmatic Approach. [Internet] [Doctoral dissertation]. Vanderbilt University; 2011. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/1803/12061.
Council of Science Editors:
Balasubramanian DA. Behavioral Semantics of Modeling Languages: A Pragmatic Approach. [Doctoral Dissertation]. Vanderbilt University; 2011. Available from: http://hdl.handle.net/1803/12061
30.
Mohammad Gholizadeh, Hamid.
A Query Structured Model Transformation Approach.
Degree: PhD, 2017, McMaster University
URL: http://hdl.handle.net/11375/21976
► Model Driven Engineering (MDE) has gained a considerable attention in the software engineering domain in the past decade. MDE proposes shifting the focus of the…
(more)
▼ Model Driven Engineering (MDE) has gained a considerable attention in the software engineering domain in the past decade. MDE proposes shifting the focus of the engineers from concrete artifacts (e.g., code) to more abstract structures (i.e., models). Such a change allows using the human intelligence more efficiently in engineering software products. Model Transformation (MT) is one of the key operations in MDE and plays a critical role in its successful application. The current MT approaches, however, usually miss either one or both of the two essential features: 1) declarativity in the sense that the MT definitions should be expressed at a sufficiently high level of abstraction, and 2) formality in the sense that the approaches should be based on precise underlying semantics. These two features are both critical in effectively managing the complexity of a network of interrelated models in an MDE process. This thesis tackles these shortcomings by promoting a declarative MT approach that is built on mathematical foundations. The approach is called Query Structured Transformation (QueST) as it proposes a structured orchestration of diagrammatic queries in the MT definitions. The aim of the thesis is to make the QueST approach –that is based on formal foundations– accessible to the MDE community. This thesis first motivates the necessity of having declarative formal approaches by studying the variety of model synchronization scenarios in the networks of interrelated models. Then, it defines a diagrammatic query framework (DQF) that formulates the syntax and the semantics of the QueST collection-level diagrammatic operations. By a detailed comparison of the QueST approach and three rule-based MT approaches (ETL, ATL, and QVT-R), the thesis shows the way QueST contributes to the development of the following aspects of MT definitions: declarativity, modularity, incrementality, and logical analysis of MT definitions.
Thesis
Doctor of Philosophy (PhD)
Advisors/Committee Members: Maibaum, Tom, Computing and Software.
Subjects/Keywords: Model Transformation; Diagrammatic Queries; Model Synchronization Taxonomy; Formal Methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Mohammad Gholizadeh, H. (2017). A Query Structured Model Transformation Approach. (Doctoral Dissertation). McMaster University. Retrieved from http://hdl.handle.net/11375/21976
Chicago Manual of Style (16th Edition):
Mohammad Gholizadeh, Hamid. “A Query Structured Model Transformation Approach.” 2017. Doctoral Dissertation, McMaster University. Accessed January 18, 2021.
http://hdl.handle.net/11375/21976.
MLA Handbook (7th Edition):
Mohammad Gholizadeh, Hamid. “A Query Structured Model Transformation Approach.” 2017. Web. 18 Jan 2021.
Vancouver:
Mohammad Gholizadeh H. A Query Structured Model Transformation Approach. [Internet] [Doctoral dissertation]. McMaster University; 2017. [cited 2021 Jan 18].
Available from: http://hdl.handle.net/11375/21976.
Council of Science Editors:
Mohammad Gholizadeh H. A Query Structured Model Transformation Approach. [Doctoral Dissertation]. McMaster University; 2017. Available from: http://hdl.handle.net/11375/21976
◁ [1] [2] [3] [4] [5] … [14] ▶
. 
Open Access Theses and Dissertations
