Loading...
Search for:
formal-methods
0.006 seconds
Total 38 records
Derivation of Z functional input/output refinement proof rules
, Article ICEIE 2010 - 2010 International Conference on Electronics and Information Engineering, Proceedings, 1 August 2010 through 3 August 2010 ; Volume 1 , August , 2010 , Pages V1209-V1213 ; 9781424476800 (ISBN) ; Mirian Hosseinabadi, S. H ; Sharif University of Technology
2010
Abstract
In this paper, we derive Z input/output data refinement rules, including forwards and backwards rules, for the case in which the retrieve schemas are total functions when viewed as relations from the concrete to abstract variables. In practice, the relation between the abstract and concrete variables is often functional. Therefore, the use of the functional input/output refinement rules will reduce the cost and duration of the software development because the proof of the consistency of the abstract and concrete specifications is more easily demonstrated
A survey of syntax and semantics frameworks of modeling languages
, Article Proceedings of the 2009 2nd International Conference on Computer Science and Its Applications, CSA 2009 ; 2009 ; 9781424449460 (ISBN) ; Habibi, J ; Sharif University of Technology
Abstract
Modeling languages as programming languages need precise and unambiguous semantics to be used appropriately, the formal semantics is significant for designing CASE tools and model verification. Several approaches have been used throughout these years to describe the semantics of modeling languages, but in spite of programming languages, these semantics frameworks are not used in large scale for modeling languages. This paper reviews the history of developments on semantics frameworks for modeling languages. © 2009 IEEE
Generation of database schemas from Z specifications
, Article IEEE International Conference on Electro Information Technology, 15 May 2011 through 17 May 2011, Mankato, MN ; 2011 ; 21540357 (ISSN) ; Mirian Hosseinabadi, S. H ; IEEE Region 4 (R4) ; Sharif University of Technology
2011
Abstract
Automatic translation of a high-level specification language to an executable implementation would be highly useful in maximizing the benefits of formal methods. We will introduce a set of translation functions to fill the specification-implementation gap in the domain of database applications. Because the mathematical foundation of Z has many properties in common with SQL, a direct mapping from Z to SQL structures can be found. We derive a set of translation functions from Z to SQL for the generation of a database. The proposed methodology results in reducing the expenses and duration of the software development, and also, prevents the errors originated from the manual translation of...
Modeling security protocols using operational semantics
, Article ICEIT 2010 - 2010 International Conference on Educational and Information Technology, Proceedings, 17 September 2010 through 19 September 2010, Chongqing ; Volume 3 , 2010 , Pages V3179-V3185 ; 9781424480340 (ISBN) ; Mahrooghi, H ; Movaghar, A ; Faraahi, A ; Sharif University of Technology
2010
Abstract
In this paper we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analyzing the Needham-Schroeder-Lowe protocol
Using formal methods in component based software development
, Article 2008 International Conference on Systems, Computing Sciences and Software Engineering, SCSS 2008, Part of the International Joint Conferences on Computer, Information, and Systems Sciences, and Engineering, CISSE 2008, 5 December 2013 through 13 December 2013 ; 2010 , Pages 429-432 ; 9789048136575 (ISBN) ; Shirali Shahreza, M ; Sharif University of Technology
2010
Abstract
Reusing the programs which have already been developed can shorten the production time and reduce costs and expenses. One of the important issues in software reuse is finding a program or a program component in a program library which has been already developed and using it in the new program. In view of precision and automation that formal methods can provide, we can use formal methods in retrieval appropriate components from the software libraries. In this paper, some of the works done in the field of retrieval of the components from the libraries by the help of formal methods have been surveyed and reviewed
Determinacy in discrete-bidding infinite-duration games
, Article Logical Methods in Computer Science ; Volume 17, Issue 1 , 2021 , Pages 10:1-10:23 ; 18605974 (ISSN) ; Avni, G ; Henzinger, T. A ; Sharif University of Technology
Logical Methods in Computer Science
2021
Abstract
In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent,...
Determinacy in discrete-bidding infinite-duration games
, Article Logical Methods in Computer Science ; Volume 17, Issue 1 , 2021 , Pages 10:1-10:23 ; 18605974 (ISSN) ; Avni, G ; Henzinger, T. A ; Sharif University of Technology
Logical Methods in Computer Science
2021
Abstract
In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent,...
Arithmetic circuits verification without looking for internal equivalences
, Article 2008 6th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'08, Anaheim, CA, 5 June 2008 through 7 June 2008 ; 2008 , Pages 7-16 ; 9781424424177 (ISBN) ; Alizadeh, B ; Fujita, M ; Sharif University of Technology
2008
Abstract
In this paper, we propose a novel approach to extract a network of half adders from the gate-level net-list of an addition circuit while no internal equivalences exist. The technique begins with a gatelevel net-list and tries to map it into word-level adders based on an efficient bit-level adder representation. It will be shown that the proposed technique is suitable for several gate-level architectures of multipliers, as it extracts adder components in a step-wise method. This approach can also be generalized to other arithmetic circuits. In order to evaluate the effectiveness of our approach, we run it on several arithmetic circuits and compare experimental results with those of...
Formal Verification of Anonymous Communication Protocols
, M.Sc. Thesis Sharif University of Technology ; Ramezanian, Rasool (Supervisor)
Abstract
One of the biggest challenges in online communication is privacy of individuals. Although anonymous communication (AC) protocols has been the subject of several security and anonymity analyses recently, there are still few frameworks for analyzing such complex systems (e.g. Tor) and their anonymity properties in a unified manner. In this study, an overview of anonymity features and techniques will be discussed by examining various protocols that provide undetectable network communication. Afterwards, the Tor network is described more precisely. Furthermore, the literature of formal methods is briefly reviewed, and the Universal Composable (UC) framework for the analysis of cryptography...
Description and Analysis of Security Protocol by Universal Composability Framework
, M.Sc. Thesis Sharif University of Technology ; Ramezanian, Rasoul (Supervisor)
Abstract
Security protocols may be provable secure when used alone, but these protocols lose their security under composition operation. Universal Composition framework (UC) is a tool for analyzing security protocols under composition. UC framework guarantees that the cryptographic protocols keep their security under this composition operation. In this paper we state a modeling for key-evolving signature protocol within the UC framework as a case study. To do this, the ideal functionality is proposed for key-evolving signature scheme that keeps the security requirements of this scheme. Finally, we show that UC definition of security is equivalent to definition of security which is termed here as...
Design Patterns for Agent-Oriented Software Engineering, and Formalizing Design Patterns
, M.Sc. Thesis Sharif University of Technology ; Ramezanian, Rasoul (Supervisor)
Abstract
Agent-Oriented Software Engineering is one of the novel and growing paradigms in computer science, which provides systematic approaches for analysis, designing, implementation and maintenance of multi-agent systems. Agents are the main entities of the agent-oriented software systems. Agents are autonomous and behave flexibly and intelligently. This paradigm is appropriate for developing open, complex, flexible and distributed systems. Design pattern is a general reusable solution to a commonly occurring problem within a specific context in software design. Using patterns in software design has many benefits such as increasing the quality and robustness of the software. Regarding the fact...
Analysis of End-to-End Electronic Voting Systems
, M.Sc. Thesis Sharif University of Technology ; Jalili, Rasool (Supervisor)
Abstract
End-to-end electronic voting protocols for electronic voting systems are used to hold a secure election with the two features of anonymity and verifiability. Verifiable mixnets are a fundamental element of electronic voting systems, which can keep the voters anonymous by mixing their votes, and provide a verifiability mechanism to prove their performance correctness. As the design of electronic voting protocols is error-prone, researchers consider the use of mathematics-based and systematic methods for their analysis. Therefore, based on formal methods and the process algebra approach, several studies have been conducted to analyze these systems, but none have properly analyzed verifiable...
Refning Object Oriented Formal Specifcation To Object Oriented Code
, M.Sc. Thesis Sharif University of Technology ; Mirian Hosseinabadi, Hassan (Supervisor)
Abstract
The presented work provides a calculus for refining an object oriented formal specification to an object oriented code. A refinement calculus provides a framework to produce executable code from a specification while preserving its correctness. Eiffel Refinement Calculus is the most complete work in this domain which is studied in this research.
The Formal specification language which is considered for this purpose is .JML to specify executable code in .Java language. For this calculus some refinement laws are pre- sented and their proofs is given by weakest precondition predicate transformer, a work which was not considered in Eiffel Refinement Calculus. The constructs which are used in...
The Formal specification language which is considered for this purpose is .JML to specify executable code in .Java language. For this calculus some refinement laws are pre- sented and their proofs is given by weakest precondition predicate transformer, a work which was not considered in Eiffel Refinement Calculus. The constructs which are used in...
Automatic checking of eligibility in electronic voting protocolsusing mCRL2
, Article 2011 CSI International Symposium on Computer Science and Software Engineering, CSSE 2011, 15 June 2011 through 16 June 2011 ; June , 2011 , Pages 62-68 ; 9781612842073 (ISBN) ; Mahrooghi, H. R ; Jalili, R ; Sharif University of Technology
2011
Abstract
Eligibility is one of the important security properties which must be satisfied in electronic voting systems. This property refers to legitimacy of voters and their right to vote only once. Due to insufficiency of an observational analysis to guarantee this property, formal methods are recently used to build trust on sensitive systems such as e-voting for all the involved parties. This paper reports our attempt to automatically check the eligibility property in electronic voting systems using the model checking approach. ThemCRL2 language and its toolset are also used to achieve such a checking. Two protocols, FOO92 and Lee&Kim, are modeled as case studies
High-throughput stream categorization and intrusion detection on GPU
, Article 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010, 26 July 2010 through 28 July 2010 ; August , 2010 , Pages 81-84 ; 9781424478859 (ISBN) ; Eslamiy, H ; Totoniy, E ; Khademy, A ; Sharif University of Technology
Abstract
We present a design and implementation of a high-throughput deep packet inspection performing both stream categorization and intrusion detection on GPU platform using CUDA. This implementation is capable of matching 64 ethernet packet streams against 25 given regular expressions at 524 Mb/s rate on a computer system with GeForce GTX 295 graphic card
A rigorous security analysis of a decentralized electronic voting protocol in the universal composability framework
, Article Journal of Information Security and Applications ; Volume 43 , 2018 , Pages 99-109 ; 22142134 (ISSN) ; Rezaei Aliabadi, M ; Sharif University of Technology
Elsevier Ltd
2018
Abstract
Designing an efficient and secure electronic voting (e-voting) protocol without the presence of trusted authorities, known as decentralized voting protocols, is one of the most interesting and challenging problems in cryptography. In these protocols the outcome of the protocol is computed by voters collaborating with each other. We provide a rigorous proof of security of a decentralized e-voting protocol proposed by Khader et al. in the Universal Composability (UC) Framework. This protocol is the state-of-the-art decentralized e-voting protocol in terms of efficiency and security, whose security has only been justified against a set of desired properties required in e-voting protocols. For...
High-level optimization of integer multipliers over a finite bit-width with verification capabilities
, Article 2009 7th IEEE-ACM International Conference on Formal Methods and Models for Co-Design, MEMOCODE '09, Cambridge, MA, 13 July 2009 through 15 July 2009 ; 2009 , Pages 56-65 ; 9781424448067 (ISBN) ; Tabandeh, M ; Alizadeh, B ; Fujita, M ; Sharif University of Technology
2009
Abstract
Integer multipliers with finite output bit-widths are widely used in many Digital Signal Processing (DSP) applications. In such circuits high-level optimizations like Residue Number System (RNS) can be utilized to achieve more efficient architectures compared to the conventional binary representations. This paper presents an efficient high-level Don't-Care Optimization (DC-Opt) method for integer multipliers and in general Multiply Accumulator (MAC) units when the output result is limited to a finite bit-width. This high-level optimization approach can then be combined with logic optimizations at gate-level. Experimental results have shown major improvements in terms of area and latency...
Determinacy in discrete-bidding infinite-duration games
, Article 30th International Conference on Concurrency Theory, CONCUR 2019, 27 August 2019 through 30 August 2019 ; Volume 140 , 2019 ; 18688969 (ISSN); 9783959771214 (ISBN) ; Avni, G ; Henzinger, T. A ; Sharif University of Technology
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
2019
Abstract
In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent,...
Magnifier: a compositional analysis approach for autonomous traffic control
, Article IEEE Transactions on Software Engineering ; 2021 ; 00985589 (ISSN) ; Sirjani, M ; Khamespanah, E ; Baier, C ; Movaghar, A ; Sharif University of Technology
Institute of Electrical and Electronics Engineers Inc
2021
Abstract
Autonomous traffic control systems are large-scale systems with critical goals. To satisfy expected properties, these systems adapt themselves to possible changes in their environment and in the system itself. The adaptation may result in further changes propagated throughout the system. For each change and its consequent adaptation, assuring the satisfaction of properties of the system at runtime is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on an...
Formal Verification of Timed Security Protocols
, M.Sc. Thesis Sharif University of Technology ; Izadi, Mohammad (Supervisor)
Abstract
Security protocols assure the security of the communications in computer systems using techniques such as cryptographic primitives. However, the usage of such protocols is faced by the lack of fault tolerance, where a minor disruption could cause a destructive damage. Therefore, there is a requirement to assess the reliability of these protocols. In this thesis model checking of timed security protocols is done. Model checking process includes steps that will be modeling protocol with high level and human readable specification language named THLPSL and converting this specification to special kind of timed automata named XTA and model checking will be done with UPPAAL verification tool. We...