Página 1 dos resultados de 55 itens digitais encontrados em 0.008 segundos

Simulation and formal verification of industrial systems controllers

Machado, José Mendes; Seabra, Eurico; Campos, J. Creissac; Oliveira, Filomena; Leão, Celina Pinto
Fonte: Associação Brasileira de Engenharia e Ciências Mecânicas (ABCM) Publicador: Associação Brasileira de Engenharia e Ciências Mecânicas (ABCM)
Tipo: Artigo de Revista Científica
Publicado em //2008 POR
Relevância na Pesquisa
36.31%
Actually, the safety control is one of the most important aspects studied by the international researchers, in the field of design and development of automated production systems due to social (avoid work accidents, ...), economics (machine stop time reduction, increase of productivity,...) and technological aspects (less risks of damage of the components,...). Some researchers of the Engineering School of University of Minho are also studying these aspects of safety control, using simulation and modelchecking techniques in the development of Programmable Logic Controllers (PLC) programs. The techniques currently used for the guarantee of automated production systems control safety are the Simulation and the Formal Verification. If the Simulation is faster to execute, has the limitation of considering only some system behavior evolution scenarios. Using Formal Verification it exists the advantage of testing all the possible system behavior evolution scenarios but, sometimes, it exists the limitation of the time necessary for the attainment of formal verification results. In this paper it is shown, as it is possible, and desirable, to conciliate these two techniques in the analysis of PLC programs. With the simultaneous use of these two techniques...

Automated Verification of Shape and Size

Nguyen, Huu Hai; David, Cristina; Qin, Shengchao; Chin, Wei Ngan
Fonte: MIT - Massachusetts Institute of Technology Publicador: MIT - Massachusetts Institute of Technology
Tipo: Artigo de Revista Científica Formato: 162917 bytes; application/pdf
EN
Relevância na Pesquisa
46.16%
Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system.; Singapore-MIT Alliance (SMA)

Towards automated derivation in the theory of allegories

Glanfield, Joel.
Fonte: Brock University Publicador: Brock University
Tipo: Electronic Thesis or Dissertation
ENG
Relevância na Pesquisa
35.8%
We provide an algorithm that automatically derives many provable theorems in the equational theory of allegories. This was accomplished by noticing properties of an existing decision algorithm that could be extended to provide a derivation in addition to a decision certificate. We also suggest improvements and corrections to previous research in order to motivate further work on a complete derivation mechanism. The results presented here are significant for those interested in relational theories, since we essentially have a subtheory where automatic proof-generation is possible. This is also relevant to program verification since relations are well-suited to describe the behaviour of computer programs. It is likely that extensions of the theory of allegories are also decidable and possibly suitable for further expansions of the algorithm presented here.

Bangladesh - Revenue Mobilization Program for Results: VAT Improvement Program Technical Assessment

World Bank
Fonte: Washington, DC Publicador: Washington, DC
EN_US
Relevância na Pesquisa
36%
This operation will support the VAT Improvement Program to assist the National Board of Revenue (NBR) in streamlining and modernizing Value Added Tax (VAT) operations and establishing an integrated VAT Management System for the purposes of implementing the new regime. The primary focus of the program is to prepare the administration to be able to administer the new VAT, which is to be introduced in July 2015. The new VAT Act, 2012 provides for a modern VAT scheme based on few exemptions and self-assessment. The Act provides the legal basis for the new VAT administration, and the impetus for a shift from manual to automated and modernized core tax business processing. The program is part of the government s broader tax reform agenda as articulated in the Tax Modernization Plan 2011-16 (endorsed by Parliament in June 2011), which envisages policy and institutional reform alongside a program for automating NBR operations to improve services to taxpayers, reduce administrative costs for taxpayers, and improve compliance. The VAT improvement program aims to widen the tax base by enhancing voluntary compliance...

Automated behavior property verification tool

Leo, John K.
Fonte: Monterey, California. Naval Postgraduate School Publicador: Monterey, California. Naval Postgraduate School
Tipo: Tese de Doutorado Formato: xiv, 141 p. : col. ill. ;
Relevância na Pesquisa
36.08%
Computer generated forces (CGF) simulations have entities as actors in their simulation. A type of CGF in which the entities have limited autonomy is semi-automated forces (SAF). The SAF system for this thesis research is OneSAF, a near real-time SAF that offers raw data collection of the entities in a particular simulation scenario. The data collection files vary in size from 500 kilobytes to larger than four gigabytes. Entity behavior property verification (BPV) is an integral part of SAF simulation software testing. The purpose for this research is to provide immediate feedback to the system user/developer as to what an entity had done in a scenario. From the simulation point of view, it provides answers to questions like "Did the entity route shortest distance to destination?" From the developer's point of interest, the BPV can provide insight to flaws in the model, such as a vehicle crossing a river where a bridge does not exist. Automated BPV (ABPV) takes one step further by minimizing "hard coding" of tools that process collection files. ABPV allows portability of the product of this thesis to other systems. ABPV Tools (ABPVT) of this thesis is designed to run in Linux and Windows and will be included in future distributions of OneSAF as an intricate part of the testing suite.; US Navy (USN) author.

Automated verification of model-based programs under uncertainty

Mahtab, Tazeen, 1981-
Fonte: Massachusetts Institute of Technology Publicador: Massachusetts Institute of Technology
Tipo: Tese de Doutorado Formato: 91 p.; 4340049 bytes; 4350214 bytes; application/pdf; application/pdf
EN_US
Relevância na Pesquisa
26.16%
Highly robust embedded systems have been enabled through software executives that have the ability to reason about their environment. Those that employ the model-based autonomy paradigm automatically diagnose and plan future actions, based on models of themselves and their environment. This includes autonomous systems that must operate in harsh and dynamic environments, like, deep space. Such systems must be robust to a large space of possible failure scenarios. This large state space poses difficulties for traditional scenario-based testing, leading to a need for new approaches to verification and validation. We propose a novel verification approach that generates an analysis of the most likely failure scenarios for a model-based program. By finding only the lost likely failures, we increase the relevance and reduce the quantity of information the developer must examine. First, we provide the ability to verify a stochastic system that encodes both off-nominal and nominal scenarios. We incorporate uncertainty into the verification process by acknowledging that all such programs may fail, but in different ways, with different likelihoods. The verification process is one of finding the most likely executions that fail the specification. Second...

Toward a Security Domain Model for Static Analysis and Verification of Information Systems

Shaffer, Alan; Auguston, Mikhail; Irvine, Cynthia E.; Levin, Tim.
Fonte: OOPSLA Workshop on Domain-Specific Modelling (DSM '07). Montreal, Canada. Publicador: OOPSLA Workshop on Domain-Specific Modelling (DSM '07). Montreal, Canada.
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
56.17%
OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada.; Evaluation of high assurance secure computer systems requires that they be designed, developed, verified and tested using rigorous processes and formal methods. The evaluation process must include correspondence between security policy objectives, security specifications, and program implementation. This research presents an approach to the verification of programs represented in a specialized Implementation Modeling Language (IML) using a formal security Domain Model (DM). The DM is comprised of an invariant part, which defines the generic concepts of program state, information flow, and other security properties; and a variable part, specifying the behavior of the target program. The DM is written using the Alloy formal specification language, and its verification is accomplished using the Alloy Analyzer tool. It was found that, by separating the structural framework of the security policy from the semantics of the target program, efficiency of the Alloy Analyzer in detecting execution paths that violate the security properties specified in the DM is significantly improved.

A Security Domain Model to Assess Software for Exploitable Covert Channels

Auguston, Mikhail; Levin, Timothy; Shaffer, Alan; Irvine, Cynthia E.
Fonte: Association for Computing Machinery (ACM) Publicador: Association for Computing Machinery (ACM)
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
45.94%
Within a multilevel secure (MLS) system, trusted subjects are granted privileges to perform operations that are not possible by ordinary subjects controlled by mandatory access control (MAC) policy enforcement mechanisms. These subjects are trusted not to conduct malicious activity or degrade system security. We present a formal definition for trusted subject behaviors, which depends upon a representation of information flow and control dependencies generated during a program execution. We describe a security Domain Model (DM) designed in the Alloy specification language for conducting static analysis of programs to identify illicit information flows, access control flaws and covert channel vulnerabilities. The DM is compiled from a representation of a target program, written in an intermediate Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to detect potential security policy violations in the target program. In particular, since the operating system upon which the trusted subject runs has limited ability to control its actions, static analysis of trusted subject operations can contribute to the security of the system.

Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems

Kovacs, Laura; Pugliese, Rosario; Tiezzi, Francesco
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 09/08/2011
Relevância na Pesquisa
26.17%
This volume contains the final and revised versions of the papers presented at the 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011). The workshop was held in Reykjavik, Iceland, on June 9, 2011, as part of DisCoTec 2011. The aim of the WWV workshop series is to provide an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools drawn from Rule-based programming, Software engineering, Formal methods and Web-oriented research. Nowadays, indeed, many companies and institutions have diverted their Web sites into interactive, completely-automated, Web-based applications for, e.g., e-business, e-learning, e-government, and e-health. The increased complexity and the explosive growth of Web systems have made their design and implementation a challenging task. Systematic, formal approaches to their specification and verification can permit to address the problems of this specific domain by means of automated and effective techniques and tools. In response to this year's call for papers, we received 9 paper submissions. The Program Committee of WWV 2011 collected three reviews for each paper and held an electronic discussion leading to the selection of 7 papers for presentation at the workshop. In addition to the selected papers...

Automated Benchmarking of Incremental SAT and QBF Solvers

Egly, Uwe; Lonsing, Florian; Oetsch, Johannes
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
26.05%
Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers. Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program. We illustrate our approach by different hardware verification problems for SAT and QBF solvers.; Comment: camera-ready version (8 pages + 2 pages appendix), to appear in the proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), LNCS, Springer, 2015

Generalization Strategies for the Verification of Infinite State Systems

Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio; Senni, Valerio
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 05/10/2011
Relevância na Pesquisa
26.18%
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools. To appear in Theory and Practice of Logic Programming (TPLP).; Comment: 24 pages...

A Program Logic for Verifying Secure Routing Protocols

Chen, Chen; Jia, Limin; Xu, Hao; Luo, Cheng; Zhou, Wenchao; Loo, Boon Thau
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 13/10/2015
Relevância na Pesquisa
26.09%
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a declarative specification language for secure routing protocols for verifying properties of these protocols. We prove invariant properties of SANDLog programs that run in an adversarial environment. As a step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations. VCGen is integrated into a compiler for SANDLog that can generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols can be carried out in this unified framework. To validate our framework, we encoded several proposed secure routing mechanisms in SANDLog, verified variants of path authenticity properties by manually discharging the generated verification conditions in Coq, and generated executable code based on SANDLog specification and ran the code in simulation.

Loop invariants: analysis, classification, and examples

Furia, Carlo A.; Meyer, Bertrand; Velder, Sergey
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
26.05%
Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a "loop invariant". Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs. We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns, and presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on "domain theory". It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.

Proceedings 8th International Workshop on Automated Specification and Verification of Web Systems

Silva, Josep; Tiezzi, Francesco
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 21/10/2012
Relevância na Pesquisa
26.1%
This volume contains the final and revised versions of the papers presented at the 8th International Workshop on Automated Specification and Verification of Web Systems (WWV 2012). The workshop was held in Stockholm, Sweden, on June 16, 2012, as part of DisCoTec 2012. WWV is a yearly workshop that aims at providing an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools drawn from Rule-based programming, Software engineering, Formal methods and Web-oriented research. WWV has a reputation for being a lively, friendly forum for presenting and discussing work in progress. The proceedings have been produced after the symposium to allow the authors to incorporate the feedback gathered during the event in the published papers. All papers submitted to the workshop were reviewed by at least three Program Committee members or external referees. The Program Committee held an electronic discussion leading to the acceptance of all papers for presentation at the workshop. In addition to the presentation of the contributed papers, the scientific programme included the invited talks by two outstanding speakers: Rocco De Nicola (IMT, Institute for Advanced Studies Lucca...

Practical Verification of Decision-Making in Agent-Based Autonomous Systems

Dennis, Louise A.; Fisher, Michael; Lincoln, Nicholas K.; Lisitsa, Alexei; Veres, Sandor M.
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 09/10/2013
Relevância na Pesquisa
26.01%
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.; Comment: Submitted to Journal of Automated Software Engineering

An Immune System Inspired Approach to Automated Program Verification

Banerjee, Soumya
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 15/05/2009
Relevância na Pesquisa
66.3%
An immune system inspired Artificial Immune System (AIS) algorithm is presented, and is used for the purposes of automated program verification. Relevant immunological concepts are discussed and the field of AIS is briefly reviewed. It is proposed to use this AIS algorithm for a specific automated program verification task: that of predicting shape of program invariants. It is shown that the algorithm correctly predicts program invariant shape for a variety of benchmarked programs.

Compositional Safety Verification with Max-SMT

Brockschmidt, Marc; Larraz, Daniel; Oliveras, Albert; Rodriguez-Carbonell, Enric; Rubio, Albert
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
36.16%
We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition $\varphi$, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies $\varphi$. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures to prove the validity of a precondition, using the obtained intermediate results to restrict the search space for further proof attempts. As only small program parts need to be handled at a time, our method is scalable and distributable. The derived conditions can be viewed as implicit contracts between different parts of the program, and thus enable an incremental program analysis.; Comment: Extended technical report version of the conference paper at FMCAD'15

Automated verification of weak equivalence within the SMODELS system

Janhunen, Tomi; Oikarinen, Emilia
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 25/08/2006
Relevância na Pesquisa
26.06%
In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an answer set solver as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To ease answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs P and Q under consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence of P and Q. The method is developed here in a slightly more general setting by taking the visibility of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called lpeq that enables the verification of weak equivalence within the smodels system using the same search engine as for the search of models. Our experiments with lpeq and smodels suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.; Comment: 48 pages...

Local Termination: theory and practice

Endrullis, Joerg; de Vrijer, Roel; Waldmann, Johannes
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Relevância na Pesquisa
26.08%
The characterisation of termination using well-founded monotone algebras has been a milestone on the way to automated termination techniques, of which we have seen an extensive development over the past years. Both the semantic characterisation and most known termination methods are concerned with global termination, uniformly of all the terms of a term rewriting system (TRS). In this paper we consider local termination, of specific sets of terms within a given TRS. The principal goal of this paper is generalising the semantic characterisation of global termination to local termination. This is made possible by admitting the well-founded monotone algebras to be partial. We also extend our approach to local relative termination. The interest in local termination naturally arises in program verification, where one is probably interested only in sensible inputs, or just wants to characterise the set of inputs for which a program terminates. Local termination will be also be of interest when dealing with a specific class of terms within a TRS that is known to be non-terminating, such as combinatory logic (CL) or a TRS encoding recursive program schemes or Turing machines. We show how some of the well-known techniques for proving global termination...

Proceedings of the Third International Workshop on Verification and Program Transformation

Lisitsa, Alexei; Nemytykh, Andrei P.; Pettorossi, Alberto
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 05/12/2015
Relevância na Pesquisa
36.17%
This volume contains the papers selected among those which were presented at the 3rd International Workshop on Verification and Program Transformation (VPT 2015) held in London, UK, on April 11th, 2015. Previous editions of the Workshop were held at Saint-Petersburg (Russia) in 2013, and Vienna (Austria) in 2014. Those papers show that methods and tools developed in the field of program transformation such as partial evaluation and fold/unfold transformations, and supercompilation, can be applied in the verification of software systems. They also show how some program verification methods, such as model checking techniques, abstract interpretation, SAT and SMT solving, and automated theorem proving, can be used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.