-
Autonomous System Safety Properties with Multi-Machine Hybrid Event-B
Authors:
Richard Banach
Abstract:
Event-B is a well known methodology for the verified design and development of systems that can be characterised as discrete transition systems. Hybrid Event-B is a conservative extension that interleaves the discrete transitions of Event-B (assumed to be temporally isolated) with episodes of continuously varying state change. While a single Hybrid Event-B machine is sufficient for applications wi…
▽ More
Event-B is a well known methodology for the verified design and development of systems that can be characterised as discrete transition systems. Hybrid Event-B is a conservative extension that interleaves the discrete transitions of Event-B (assumed to be temporally isolated) with episodes of continuously varying state change. While a single Hybrid Event-B machine is sufficient for applications with a single locus of control, it will not do for autonomous systems, which have several loci of control by default. Multi-machine Hybrid Event-B is designed to allow the specification of systems with several loci of control. The formalism is succinctly surveyed, pointing out the subtle semantic issues involved. The multi-machine formalism is then used to specify a relatively simple incident response system, involving a controller, two drones and three responders, working in a partly coordinated and partly independent fashion to manage a putative hazardous scenario.
△ Less
Submitted 21 November, 2024;
originally announced November 2024.
-
Blockchain-enhanced Integrity Verification in Educational Content Assessment Platform: A Lightweight and Cost-Efficient Approach
Authors:
Talgar Bayan,
Richard Banach,
Askar Nurbekov,
Makhmud Mustafabek Galy,
Adi Sabyrbayev,
Zhanat Nurbekova
Abstract:
The growing digitization of education presents significant challenges in maintaining the integrity and trustworthiness of educational content. Traditional systems often fail to ensure data authenticity and prevent unauthorized alterations, particularly in the evaluation of teachers' professional activities, where demand for transparent and secure assessment mechanisms is increasing. In this contex…
▽ More
The growing digitization of education presents significant challenges in maintaining the integrity and trustworthiness of educational content. Traditional systems often fail to ensure data authenticity and prevent unauthorized alterations, particularly in the evaluation of teachers' professional activities, where demand for transparent and secure assessment mechanisms is increasing. In this context, Blockchain technology offers a novel solution to address these issues. This paper introduces a Blockchain-enhanced framework for the Electronic Platform for Expertise of Content (EPEC), a platform used for reviewing and assessing educational materials. Our approach integrates the Polygon network, a Layer-2 solution for Ethereum, to securely store and retrieve encrypted reviews, ensuring both privacy and accountability. By leveraging Python, Flask, and Web3.py, we interact with a Solidity-based smart contract to securely link each review to a unique identifier (UID) that connects on-chain data with real-world databases. The system, containerized using Docker, facilitates easy deployment and integration through API endpoints. Our implementation demonstrates significant cost savings, with a 98\% reduction in gas fees compared to Ethereum, making it a scalable and cost-effective solution. This research contributes to the ongoing effort to implement Blockchain in educational content verification, offering a practical and secure framework that enhances trust and transparency in the digital education landscape.
△ Less
Submitted 29 September, 2024;
originally announced September 2024.
-
A Privacy-Preserving DAO Model Using NFT Authentication for the Punishment not Reward Blockchain Architecture
Authors:
Talgar Bayan,
Richard Banach
Abstract:
\This paper presents a novel decentralized autonomous organization (DAO) model leveraging non-fungible tokens (NFTs) for advanced access control and privacy-preserving interactions within a Punishment not Reward (PnR) blockchain framework. The proposed model introduces a dual NFT architecture: Membership NFTs (\(NFT_{auth}\)) for authentication and access control, and Interaction NFTs (\(NFT_{priv…
▽ More
\This paper presents a novel decentralized autonomous organization (DAO) model leveraging non-fungible tokens (NFTs) for advanced access control and privacy-preserving interactions within a Punishment not Reward (PnR) blockchain framework. The proposed model introduces a dual NFT architecture: Membership NFTs (\(NFT_{auth}\)) for authentication and access control, and Interaction NFTs (\(NFT_{priv}\)) for enabling private, encrypted interactions among participants. Governance is enforced through smart contracts that manage reputation and administer punitive measures, such as conditional identity disclosure. By prioritizing privacy, security, and deterrence over financial rewards, this model addresses key challenges in existing blockchain incentive structures, paving the way for more sustainable and decentralized governance frameworks.
△ Less
Submitted 21 May, 2024;
originally announced May 2024.
-
Exploring the Privacy Concerns in Permissionless Blockchain Networks and Potential Solutions
Authors:
Talgar Bayan,
Richard Banach
Abstract:
In recent years, permissionless blockchains have gained significant attention for their ability to secure and provide transparency in transactions. The development of blockchain technology has shifted from cryptocurrency to decentralized finance, benefiting millions of unbanked individuals, and serving as the foundation of Web3, which aims to provide the next generation of the internet with data o…
▽ More
In recent years, permissionless blockchains have gained significant attention for their ability to secure and provide transparency in transactions. The development of blockchain technology has shifted from cryptocurrency to decentralized finance, benefiting millions of unbanked individuals, and serving as the foundation of Web3, which aims to provide the next generation of the internet with data ownership for users. The rise of NFTs has also helped artists and creative workers to protect their intellectual property and reap the benefits of their work. However, privacy risks associated with permissionless blockchains have become a major concern for individuals and institutions. The role of blockchain in the transition from Web2 to Web3 is crucial, as it is rapidly evolving. As more individuals, institutions, and organizations adopt this technology, it becomes increasingly important to closely monitor the new risks associated with permissionless blockchains and provide updated solutions to mitigate them. This paper endeavors to examine the privacy risks inherent in permissionless blockchains, including Remote Procedure Call (RPC) issues, Ethereum Name Service (ENS), miner extractable value (MEV) bots, on-chain data analysis, data breaches, transaction linking, transaction metadata, and others. The existing solutions to these privacy risks, such as zero-knowledge proofs, ring signatures, Hyperledger Fabric, and stealth addresses, shall be analyzed. Finally, suggestions for the future improvement of privacy solutions in the permissionless blockchain space shall be put forward.
△ Less
Submitted 1 May, 2023;
originally announced May 2023.
-
Formalising the Continuous/Discrete Modeling Step
Authors:
Richard Banach,
Huibiao Zhu,
Wen Su,
Runlei Huang
Abstract:
Formally capturing the transition from a continuous model to a discrete model is investigated using model based refinement techniques. A very simple model for stopping (eg. of a train) is developed in both the continuous and discrete domains. The difference between the two is quantified using generic results from ODE theory, and these estimates can be compared with the exact solutions. Such result…
▽ More
Formally capturing the transition from a continuous model to a discrete model is investigated using model based refinement techniques. A very simple model for stopping (eg. of a train) is developed in both the continuous and discrete domains. The difference between the two is quantified using generic results from ODE theory, and these estimates can be compared with the exact solutions. Such results do not fit well into a conventional model based refinement framework; however they can be accommodated into a model based retrenchment. The retrenchment is described, and the way it can interface to refinement development on both the continuous and discrete sides is outlined. The approach is compared to what can be achieved using hybrid systems techniques.
△ Less
Submitted 21 June, 2011;
originally announced June 2011.
