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

142
views

0
downloads

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

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.