28 research outputs found
A methodology to support UML-B model development
Get PDFUML-B is a graphical front-end for the formal method Event-B. UML-B models
are translated to Event-B for verification purpose. Modelling and proving
become difficult for complex models with many state variables and transitions.
Reducing modelling and proving effort is potential for UML-B models. Decomposition,
composition, model matching, and pattern reuse are attracting methods
to support individual team modelling, comparing, integrating, and reusing
models helping UML-B modellers and practitioners to avoid remodelling and
reduce the proof effort required to verify the correctness of the models.
Decomposition in Event-B divides a complex model into sub-parts reducing certainly
its complexity and facilitating independent modelling for the sub-parts.
Two decomposition styles exist for Event-B which are shared-event and sharedvariable.
The shared-event style has been introduced in UML-B and it is considered
suitable for synchronous message passing systems. However, the sharedvariable
style is not supported before in UML-B. In this research, a correctby-
construction method is introduced to support the shared-variable decomposition
in UML-B that is considered suitable for asynchronous shared variable
models. The proposed method is provided through three sequential phases
which are refinement-preparation, actual-decomposition, and refinement-afterdecomposition.
The provision of new notions, conditions, and rules is a significant
step to maintain the graphical semantics of UML-B and the shared variable
formalism of Event-B. We introduce refinement-preparation strategies and conditions,
actual-decomposition rules, refinement-after-decomposition conditions,
new UML-B notions, and a representation mechanism. The method is formalised
and verified via a generic proof on a theoretical level to show how the generated
semantic implicit invariants and the shared variable formalism are preserved,
and to prove that any recomposed machine is indeed correct and a refinement
of the original decomposable machine when the method phases conditions and rules are followed. The method is illustrated by a case study on the updating of
master data, in which the notions, conditions, and rules are applied.
Event-B composition is to reuse existing interacting models specifications to construct
a larger one fulfilling the complete system behaviour. In this research, a
correct-by-construction method is introduced to compose UML-B machines that
interact via the shared-variable style. This saves the modelling and proving
effort via the correct machines that are being composed. The method is provided
through steps and rules, and its correctness is verified by proving that
any composed machine is indeed correct when the method rules are followed.
The method applicability is also illustrated by the case study on the updating of
master data.
Identifying similarities between models has several benefits such as model comparison,
integration, and evolution. Several matching and comparison methods
have been done in the context of model driven software engineering. However,
matching models via a systematic method is not supported yet in UML-B. In this
work, we propose a matching method for UML-B elements based on their semantics.
This method includes variable-based, event-based, and state-machine
matching. The variable-based matching provides rules for matching UML-B
classes, attributes, states, and variables. The event-based matching provides
rules and cases for matching UML-B transitions and class-events. The statemachine
matching provides rules for matching UML-B state-machines based on
the state and transition matching rules. The matching rules are formalized by
means of the generated corresponding Event-B specifications. The correctness
of the rules is justified via preserving the compatibility of the matched statevariables
and corresponding modifying events including their matched guards
and actions. These rules are illustrated via a communication-based case study to
show their applicability.
Pattern reuse allows reusing models in constructing new ones saving the modelling
and proving effort. However, there is no systematic method in terms of
pattern reuse in UML-B. In this research, a correct-by-construction method is introduced
to support the reuse of UML-B models which is based on the Event-B
pattern reuse. The method is provided through three sequential phases which
are pattern matching, checking, and incorporation. The provision of new guidelines
and rules is necessary to preserve both the UML-B graphical semantics and
the method correctness. This is proven via a generic proof using the proofs from
the pattern that is integrated with the problem model. The proposed method reduces
certainly the modelling and proving effort by using existing models in
constructing new ones, since it is always that the proof obligations from the
pattern model do not need to be proven again during the integration between
the pattern and problem models. The method applicability is illustrated by the
communication-based case study introduced in the model matching
Software requirements prioritization tool using a hybrid technique
Get PDFRequirements Prioritization (RP) helps to discover the most desired requirements. System developers are not always fully able to implement stakeholders' requirements when time, scope and cost are limited. To solve this challenge, requirements must be prioritized. A fewprioritization techniques have been proposed but nonehasbeen automated. Furthermore, rank reversals (updating rank status whenever requirements are added or deleted) is a major limitation of existing techniques.This paper usesAHP and Cost-Value methodsfor requirement prioritization while addressing rank reversal. The techniques are able to rank every requirement basedon relative value and implementation cost. The AHP method allows an input from the system developers and system users andmakesa pair wisecomparison. The Cost value method ranks the requirements in terms ofthe ratio of value to cost. As requirements increases, human inconsistency in judgment increases.AHP calculates inconsistency and if it is less than 0.1 then stakeholdersshould consider new input values. The prioritization methods are implemented into a prioritization tool which creates a list of the prioritized requirements as output, then consequently generates a scatter plot to display relative values and implementation costs of input requirements.This tool isevaluated in terms ofefficiency (total time taken for prioritization) and ease of use
A Method for Automatic Android Malware Detection Based on Static Analysis and Deep Learning
No full textThe computers nowadays are being replaced by the smartphones for the most of the internet users around the world, and Android is getting the most of the smartphone systems' market. This rise of the usage of smartphones generally, and the Android system specifically, leads to a strong need to effectively secure Android, as the malware developers are targeting it with sophisticated and obfuscated malware applications. Consequently, a lot of studies were performed to propose a robust method to detect and classify android malicious software (malware). Some of them were effective, some were not; with accuracy below 90%, and some of them are being outdated; using datasets that became old containing applications for old versions of Android that are rarely used today. In this paper, a new method is proposed by using static analysis and gathering as most useful features of android applications as possible, along with two new proposed features, and then passing them to a functional API deep learning model we made. This method was implemented on a new and classified android application dataset, using 14079 malware and benign samples in total, with malware samples classified into four malware classes. Two major experiments with this dataset were implemented, one for malware detection with the dataset samples categorized into two classes as just malware and benign, the second one was made for malware detection and classification, using all the five classes of the dataset. As a result, our model overcomes the related works when using just two classes with F1-score of 99.5%. Also, high malware detection and classification performance was obtained by using the five classes, with F1-score of 97%
Simplicity and Beauty in Basheer’s The Inheritors of Earth
Get PDFVaikom Muhammed Basheer is a notable writer of Malayalam literature. His works are always close to nature. People can easily identify his works because of their lucid language and their inclination to nature. In his work, ‘Bhoomiyude Avakashikal’ (The Inheritors of Earth), the author tries to talk about the need of considering the animals and birds around us because they are also a part of our earth. Basheer sheds light on the truth that the entire species in this world have the same rights that man holds. Each and every living being has the equal right to live and enjoy their surroundings as human beings. If we don’t protect our nature - the vegetation and biodiversity around us - we have no future
Towards employing metrics in measuring the quality of software safety critical systems and managing their development
No full textFailures in safety critical systems have a high impact on the environment in which they are used. For that, developers usually follow specific development standards and techniques to avoid and reduce failures in such systems. Developers have to build safety critical systems considering the quality, complexity, and size factors in all the development phases beginning with the requirement gathering and ending with the maintenance and verification. In this paper, some quality models and some metrics for measuring the quality, complexity, and size of systems are explored. The metrics are classified to the development phases so that the classification indicates the degree of metrics usage in measuring the quality, complexity, and size factors in relation to the development phases. We are now working on relating the studied metrics in this paper with their impact on the development of the software safety critical system. We expect to use these metrics in the management of the development phases and processes of software safety critical systems so that a decision making could be performed based on the measurements of these metrics
A comparative study on embedding models for keyword extraction using keyBERT method
No full textKeyBERT is a method for keywords/keyphrases extraction, which has three steps. The first step is selecting candidate keywords from a text using sklearn library, the second step is the embedding operation of the text and its candidate keywords; this operation is done by BERT to get a numerical representation that represents the meanings. The third step is calculating the cosine similarity between individual keywords vectors and document vector. In this paper, we focus on the second step of KeyBERT (embedding step). Although KeyBERT has a lot of supported models for the embedding operation, there are no extensive previous comparative studies to analyze and study the effect of using different supported models in KeyBERT. We introduce a comparative study of two commonly used groups of models; the first group is sentence-transformers pretrained models, supported via the sentence-transformers library, and the second group includes the Longformer model, supported via the Hugginface Transformers library. We conduct the comparative study of models on benchmark datasets, which contain English text documents of multi-domains with different text lengths. Based on the study, we found that the Paraphrase-mpnet-base-v2 model provides the best results among all other models in keyword extraction in terms of effectiveness (f1-score, recall, precision, MAP) on all datasets, with higher efficiency (time) on short text compared with using it on long text; accordingly, we recommend using it in that context. On the other hand, the Longformer model is the most efficient/fastest in keyword extraction among all other models on all datasets and this superiority has been evident, especially in long text; accordingly, we recommend using it in that context
The measurement of safety criteria in safety critical systems
Get PDFSafety critical systems use software to meet their unctionalities. Failures in these software lead to a very high impact on the environment in which the safety critical systems are used. Several criteria are considered in safety critical systems, which are: reliability, availability, maintainability and safety. In this paper, we focus on measuring the safety criterion in safety critical systems. Safety has some factors that are: correctness, security, responsiveness and testability. Correctness is one of the most important factors of safety. Correctness also has sub-factors such as: completeness and consistency. In this paper, we investigate the safety criteria and safety measurement via two specific domains: transportation systems and business intelligent systems. Also, these criteria are employed in our developed prototype for verifying the safety criteria of safety critical systems and supporting the management of safety critical systems
Formalization in digital forensic triage for identification of malicious IoT devices
No full textConsidering the large number of devices connected to
the Internet of Things(IoT), identifying malicious devices for the
purpose of “search & seizure” remainsa critical issue for digital
investigators. Consequently, the need for techniques that
automatically identify malicious devices can speed up the process
of digital investigation. However, few conceptual approaches were
proposed to identify malicious devices during IoT forensic
investigation. To overcome that, a formal approach is proposed to
automatically triage and fingerprint IoT Malicious devices with
their respective states. It is expected that with the proposed formal
approach, investigators can simply identify malicious devices,
their states as well as determine the scope of investigation
Performance Analysis of New 2D Spatial OCDMA Encoding based on HG Modes in Multicore Fiber
No full textThis paper presents a pioneering 2D spatial Optical Code-Division Multiple Access (OCDMA) encoding system that exploits
Mode Division Multiplexing (MDM) and Multicore Fiber (MCF) technologies. This innovative approach utilizes two spatial dimensions
to enhance the performance and security of OCDMA systems. In the first dimension, we employ Hermite-Gaussian modes (HG00,
HG01, HG11) to modulate each user's signal individually. This unique approach offers a robust means of data transmission while
ensuring minimal interference among users. The second-dimension leverages MCF encoding, introducing two incoherent OCDMA
codes: the Zero Cross Correlation (ZCC) code (λc=0) and the ZFD code (λc=1). These codes are thoughtfully designed and simulated,
taking into account their cross-correlation properties to guarantee minimal interference and heightened data security. To assess the
efficiency of this novel OCDMA encoding system, we implemented simulations with three active users using the Opti system software.
At the transmitter end, each user's signal is modulated individually by their designated HG mode (HG00, HG01, HG11), resulting in
separate channels. Subsequently, at the multicore fiber, each user's data is encoded with a unique code-word, and they are directed
through specific core groups, ensuring data isolation and integrity. In this paper, the BER and eye pattern are examined with respect
to different parameters such as data rate and distance. At a distance of 5 km and data rate of 10 Gbit/s, a BER value around 10-70 is
achieve
Harris Hawk Optimization-Based Deep Neural Networks Architecture for Optimal Bidding in the Electricity Market
Get PDFIn the power sector, competitive strategic bidding optimization has become a major challenge. Digital plate-form provides a superior technical base as well as backing for the optimization’s execution. The state-of-the-art frameworks used for simulating strategic bidding decisions in deregulated electricity markets (EM’s) in this article are bi-level optimization and neural networks. In this research, we provide HHO-NN (Harris Hawk Optimization-Neural network), a novel algorithm based on Harris Hawk Optimization (HHO) that is capable of fast convergence when compared to previous evolutionary algorithms for automatically searching for meaningful multilayered perceptron neural networks (MPNNs) topologies for optimal bidding. This technique usually demands a considerable amount of time and computer resources. This method sets up the problem in multi-dimensional continuous state-action spaces, allowing market players to get precise information on the effect of their bidding judgments on the market clearing results, as well as implement more valuable bidding decisions by utilizing a whole action domain and accounting for non-convex operating principles. Due to the use of the MPNN, case studies show that the suggested methodology delivers a much larger profit than other state-of-the-art methods and has a better computational performance than the benchmark HHO technique
