Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
Interface-based specification and verification of concurrency controllers
Date
2003-09-01
Author
Bultan, Tevfik
Betin Can, Aysu
Metadata
Show full item record
This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License
.
Item Usage Stats
148
views
0
downloads
Cite This
We present a modular approach to specification and verification of concurrency controllers by decoupling their behavior and interface specifications. The behavior specification of a concurrency controller defines how its shared variables change their values whereas the interface specification defines the order in which a client thread should call its methods. We show that the concurrency controllers can be designed modularly by composing their interfaces. We separate the verification of the concurrency controllers from the verification of the threads that use them. For the verification of the concurrency controllers we use infinite state verification techniques which enable us to verify controllers with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the concurrency controller specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enable us to verify Java threads without any restrictions. We show that the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly.
URI
https://hdl.handle.net/11511/30979
Journal
Electronic Notes in Theoretical Computer Science
DOI
https://doi.org/10.1016/s1571-0661(05)80007-6
Collections
Graduate School of Informatics, Article
Suggestions
OpenMETU
Core
Linear static analysis of large structural models on pc clusters
Özmen, Semih; Toker, Kurç; Department of Civil Engineering (2009)
This research focuses on implementing and improving a parallel solution framework for the linear static analysis of large structural models on PC clusters. The framework consists of two separate programs where the first one is responsible from preparing data for the parallel solution that involves partitioning, workload balancing, and equation numbering. The second program is a fully parallel nite element program that utilizes substructure based solution approach with direct solvers. The first step of data...
Cortex-M4 optimizations for {R, M} LWE schemes
Alkım, Erdem; Bilgin, Yusuf Alper; Cenk, Murat; Gérard, François (2020-06-01)
This paper proposes various optimizations for lattice-based key encapsulation mechanisms (KEM) using the Number Theoretic Transform (NTT) on the popular ARM Cortex-M4 microcontroller. Improvements come in the form of a faster code using more efficient modular reductions, optimized small-degree polynomial multiplications, and more aggressive layer merging in the NTT, but also in the form of reduced stack usage. We test our optimizations in software implementations of Kyber and NewHope, both round 2 candidate...
Performance Evaluation of Different Real-Time Motion Controller Topologies Implemented on a FPGA
MUTLU, B. R.; Yaman, Ulaş; Dölen, Melik; Koku, Ahmet Buğra (2009-11-18)
This paper presents a comprehensive comparison of several real-time motion controller topologies implemented on a field programmable gate array (FPGA). Controller topologies are selected as proportional-integral-derivative controller with command feedforward, sliding mode controller, fuzzy controller, and a hysteresis controller. Controllers and other necessary modules are developed using Verilog HDL and they are implemented on a ML505 development board with a Xilinx Virtex-5 FPGA chip. In order to take ful...
Modular verification of synchronization with reentrant locks
Bultan, Tevfik; Yu, Fang; Betin Can, Aysu (2010-07-28)
We present a modular approach for verification of synchronization behavior in concurrent programs that use reentrant locks. Our approach decouples the verification of the lock implementation from the verification of the threads that use the lock. This decoupling is achieved using lock interfaces that characterize the allowable execution order for the lock operations. We use a thread modular verification approach to check that each thread obeys the lock interface. We verify the lock implementation assuming t...
Scalable computational steering system for vizualization of large scale CFD simulations
Tonkal, Ozan Çağrı; Pehlivan, Sercan; Sezer Uzol, Nilay; İşler, Veysi (2002-06-27)
A general-purpose computational steering system (POSSE) which can be coupled to any C/C++ simulation code, has been developed and tested with a 3-D Navier-Stokes flow solver (PUMA2). This paper illustrates how to use “computational steering” with PUMA2 to visualize CFD solutions while they are being computed, and even change the input data while it is running. In addition, the visualizations can be displayed using virtual reality facilities (such as CAVEs and RAVEs) to better understand the 3-D nature of th...
Citation Formats
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
T. Bultan and A. Betin Can, “Interface-based specification and verification of concurrency controllers,”
Electronic Notes in Theoretical Computer Science
, pp. 464–479, 2003, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/30979.