Search

At present, formal methods significantly facilitate the specification and verification of security requirements in requirement engineering, which can reduce requirement errors in the early stage of system development. Extracting formal specifications from security requirements and then evaluating the quality of the requirements are regarded as a promising solution to ensure software quality. Propositional projection temporal logic (PPTL) with a strong mathematical basis and full regular expressiveness is a suitable language for formal specifications. Inspired by natural language processing and text mining techniques, this paper designs and implements a tool, namely, NL2PPTL, to generate formal coarse‐grained and fine‐grained specifications in terms of PPTL formulas automatically. In specific, the grammatical production rules are defined to construct the syntax tree, and then, the formula is obtained by post‐order traversal of the tree. The satisfiability of the PPTL specifications can be checked utilizing PPTLSAT. In addition, the state transformation model is constructed from fine‐grained specifications, so as to discover scope conflicts and verify the security properties of the requirement case. [ABSTRACT FROM AUTHOR]

The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting statemachine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage. [ABSTRACT FROM AUTHOR]

Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications. [ABSTRACT FROM AUTHOR]

Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications. [ABSTRACT FROM AUTHOR]

The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios. [ABSTRACT FROM AUTHOR]

The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method. [ABSTRACT FROM AUTHOR]

Autonomous driving systems are crucial complicated cyber–physical systems that combine physical environment awareness with cognitive computing. Deep reinforcement learning is currently commonly used in the decision-making of such systems. However, black-box-based deep reinforcement learning systems do not guarantee system safety and the interpretability of the reward-function settings in the face of complex environments and the influence of uncontrolled uncertainties. Therefore, a formal security reinforcement learning method is proposed. First, we propose an environmental modeling approach based on the influence of nondeterministic environmental factors, which enables the precise quantification of environmental issues. Second, we use the environment model to formalize the reward machine's structure, which is used to guide the reward-function setting in reinforcement learning. Third, we generate a control barrier function to ensure a safer state behavior policy for reinforcement learning. Finally, we verify the method's effectiveness in intelligent driving using overtaking and lane-changing scenarios. [ABSTRACT FROM AUTHOR]

This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm. [ABSTRACT FROM AUTHOR]

Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this work, we consider the description of the expected behaviour of a Ladder program under the form of a timing chart, describing a scenario of execution. Our aim is to prove that the given Ladder program conforms to the expected temporal behaviour given by such a timing chart. Our approach amounts to translating the Ladder code, together with the timing chart, into a program for the Why3 environment for deductive program verification. The verification proceeds with the generation of verification conditions: mathematical formulas to be checked valid using automated theorem provers. The ultimate goal is twofold. On the one hand, by obtaining a complete proof, one verifies the conformity of the Ladder code with respect to the timing chart with a high degree of confidence. On the other hand, in the case the proof is not fully completed, one obtains a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart. [ABSTRACT FROM AUTHOR]

A formal specification is a formal description of system requirements, which is a necessity for formal verification. Due to various reasons, some systems lack of formal specifications. Compared with CTL and LTL, Propositional Projection Temporal Logic (PPTL) has a full regular expressive power. Accordingly, a pattern-library-based PPTL specification mining tool PPTLMiner [1] is able to dig out a better expression of system specification. However, there's still some room for improvement in PPTLMiner, such as deep recursion, high time complexity and space complexity, which limit the use of PPTLMiner in practical applications. Therefore, in this paper, a new PPTL specification mining approach based on Labeled Normal Form Graph (LNFG) is proposed and a supporting tool PPTLMiner+ is also developed. Finally, a specification mining example using PPTLMiner+ is given to illustrate the effectiveness and practicality of the new approach. In this example, a typical algorithm in Swarm Intelligence-Bee Colony Algorithm is selected as a target program, and the working order of EmployedBees, OnlookerBees and ScoutBees is obtained using PPTLMiner+. Further, PPTLMiner+ is compared with PPTLMiner as well as the classical linear specification mining tool Texada [2,3] in terms of time and memory to illustrate the effectiveness and practicability of the proposed method. • The framework of PPTLMiner+ and main algorithms are introduced. • A practical example of Bee Colony Algorithm is given to show how PPTLMiner+ works. • PPTLMiner+ is compared with PPTLMiner and Texada through a comparative experiment. [ABSTRACT FROM AUTHOR]

Asmart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work. [ABSTRACT FROM AUTHOR]

Nowadays, smart systems require the use of Digital Twins (DTs) for their engineering and management. Self-updating capability is a key feature in the DT technology. This raises the challenge of model inference from data collected on the system and requires a formal framework be defined, in which a system representation can be coupled with inference methods to achieve automatic model updating. While data-based process model inference is a well-known technique, the inference of a simulation model from existing knowledge and collected data is yet an unexplored area. In this paper, we first clarify and explicitly define some key elements of the terminology related to the DT concept, including model update and model inference, and we propose a framework of inference capabilities based on a formal DT specification, which formally captures the conditions for different updating capabilities and relates them. That way, on one hand, the framework enables the use of symbolic approaches to build a DT with the desired inference capability, and on the other hand, it establishes a partial order relation between inference capabilities. Through a case study, we show how the framework helps formally specifying the DT model of a mobility system toward realizing a fully capable DT. [ABSTRACT FROM AUTHOR]

• Unified Temporal Logic (UTL) is proposed which combines the characteristics of standard Linear Temporal Logic and Propositional Projection Temporal Logic. • The syntax and semantics of UTL are defined. • Logic laws in UTL are explored and some of them are semantically proved in detail. • The normal forms of UTL formulas are defined. It is also proved that each UTL formula can be equivalently transformed into a normal form. • A practical example of an elevator control system is given to show how to describe temporal properties with UTL. This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the "until" construct in LTL and the "chop" construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL. [ABSTRACT FROM AUTHOR]

The development of systems with different features becomes increasingly challenging, given the actual context, implying on the search for new approaches for requirements elicitation. One of these approaches is design thinking (DT), a process of encouraging innovation used by designers, which presents itself as fundamental in the success of new products. This scenario motivates the importance of knowing DT concepts and their techniques, which can support requirements elicitation. In this context, the authors present DTA4RE (DT assistant for requirements elicitation), a tool that suggests DT techniques for requirements elicitation, which can be used by both students and professionals who would like to adopt DT in their projects. The DTA4RE is composed of a set of 27 techniques that could be suggested to the user through a recommendation questionnaire as well as an open repository with material to support the application of these techniques. Results from the authors' two empirical studies with software engineering undergraduate and graduate students and industry professionals indicate that DTA4RE has helped in the selection of and in the learning of DT techniques when considering real problems. Most participants considered the questions from the recommendation questionnaire easy to answer, and the techniques suggested by the tool useful. [ABSTRACT FROM AUTHOR]

Requirements prioritisation deals with the ranking or classification of user requirements based on their importance. This process is central to releasing a software product with features most favoured by users. While studies have explored the efforts that are dedicated to this cause, these tend to focus on a subset of the solutions that are available in the software engineering domain. Current techniques investigated in the software engineering domain do not consider the strengths inherent in requirements prioritisation techniques developed in other disciplines (e.g. product manufacturing), a gap that should be addressed. The authors thus conducted a comprehensive systematic mapping study and critical evaluation of studies that have provided implementations of requirements prioritisation techniques across multiple disciplines (including software engineering, product manufacturing, and engineering). Among their findings, they observed that while many solutions are targeted, quite often researchers have proposed solutions that were not evaluated. Most solutions were only validated as being operational, and the attributes studied had limited effects on performance outcomes. Their evidence suggests that new techniques may address the requirements prioritisation challenge if they are inspired by hybrid approaches developed across multiple disciplines. In addition, performance trade‐offs are to be expected of such techniques, depending on their performance targets. [ABSTRACT FROM AUTHOR]

Requirement prioritisation and selection is an essential activity in modern‐day large software development. Optimal prioritisation process is critical for successful implementation and release planning in a software development project. Requirement prioritisation becomes more challenging in projects having large sets of requirements and stakeholders, having diverse perspectives resulting in irrelevancy and ambiguity during features extraction. This study aims to improve requirement prioritisation process using text mining and clustering techniques for accurate extraction of features and requirement prioritisation in multi‐stakeholder context. The proposed framework developed to avoid incompleteness in requirements and disagreement among development teams and stakeholders. Thus, the proposed framework compared with other requirement prioritisation techniques (i.e. Analytical Heretical Process, Commutative Voting and Wiegers) to highlight the significance of the proposed framework while conducting an experimental study. The results show that the proposed framework outperformed the traditional techniques and enhanced the prioritisation process with complete semantic information of extracted features and taking into account the diverse perspective of stakeholders. [ABSTRACT FROM AUTHOR]

Autonomous robotic systems are complex, hybrid, and often safety critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This article systematically surveys the state of the art in formal speci- fication and verification for autonomous robotics. Specially, it identifies and categorizes the challenges posed by, the formalisms aimed at, and the formal approaches for the specification and verification of autonomous robotics. [ABSTRACT FROM AUTHOR]

There is a significant need to give careful consideration to the Capability Maturity Model Integration (CMMI) level 2 specific practices (i.e. SP 1.1 'understand requirements' and SP 1.2 'obtain commitment to requirements'), especially in the context of small‐ and medium‐sized software development organisations, in order to assist such organisations in effectively managing their requirements engineering processes. In this study, the authors propose an abstract‐level model for each of these two specific practices as well as cover the initial evaluation of the models. In addition, necessary templates and checklists are also provided for each proposed model. The proposed models are based on a significant amount of research in software process improvement, CMMI and requirements engineering. The initial evaluation of the proposed models was executed using an expert panel review process. The results showed that the proposed models provide ease of learning and ease of use, provide stakeholder satisfaction and can be applied to small‐and medium‐sized software development organisations. It is important to highlight that this study contributes not only to the implementation of SP 1.1 and SP 1.2 of REQM process area in the context of small‐ and medium‐sized software development organisations but also to the body of knowledge on REQM. [ABSTRACT FROM AUTHOR]

Various robots are playing critical roles in many areas such as industrial manufacturing, disaster rescuing, unmanned vehicle, and science exploration. Because of the uncertain environment, changed resource, or dynamic system structure at runtime, traditional methods such as testing, model checking, and static analysis used in the development stage are not enough to ensure that the executions of robot control software satisfy specified properties. In this paper, we propose a runtime verification approach called Robots Monitor on Multilayer (RMoM) based on robot operating system (ROS) for monitoring whether the running of a robot swarm violates given temporal properties. To monitor robot system in a comprehensive manner over multiple layers, RMoM unifies resource, communication, robot, and swarm properties into a systemic, hierarchical monitoring framework. A discrete-time Metric Temporal Logic (MTL $_3$) RMoM is proposed for specifying properties with timed and parameterized characteristics in robot swarms. Then, the corresponding three-valued semantics is defined for MTL $_3$ -RMoM to generate impartial and anticipatory monitors. Moreover, a hierarchical monitoring specification language high-level specification language (HSL)-RMoM and a series of monitor construction algorithms are proposed to automatically generate monitors for MTL $_3$ -RMoM properties on ROS platform. The experiments show that the method can automatically generate the monitors for detecting properties of robot swarms. [ABSTRACT FROM AUTHOR]

This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification. [ABSTRACT FROM AUTHOR]

Many of the software development projects are not successfully finished. In many cases, this is because the software requirements were not correctly identified. One of the factors that affect the elicitation of requirements is the proper selection of requirements elicitation techniques. Even when there is a lot of literature that proposes several requirements elicitation techniques, there is no reference process model that indicates the techniques that must be applied by a requirement's engineer to elicit the requirements of a mobile application for e‐commerce. This gap covers both the elicitation of functional and non‐functional requirements. Therefore, the authors propose a new model called reference process model for requirements elicitation for e‐commerce mobile applications development (RPM‐REFEMAD), which allows the elicitation of requirements based on the use of four elicitation techniques combined in ten steps. The proposed model was applied in the requirements elicitation of two e‐commerce mobile applications in different scenarios. To visualise the results of the model, a survey was designed and applied to users/stakeholders who participated in the reference process model evaluation. The survey results indicated that RPM‐REFEMAD model helps to elicit more quality and quantity functional and non‐functional requirements, in comparison with the use of traditional requirements elicitation techniques. [ABSTRACT FROM AUTHOR]

Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies. [ABSTRACT FROM AUTHOR]

A software formal specification is useful if and only if it is consistent or non-conflictive. However, checking the correctness or consistency of a formal specification is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs. Checking the correctness and consistency of Object-Z formal specification is the main goal, which can make the specifier to get confident. Because Object-Z has inheritance property, this paper discusses it from different aspects, and focuses on the reuse of theorem proof. Finally, theorem prover Z/EVES is used to analyze and verify the Object-Z theorem proofs (semi-)automatically. [ABSTRACT FROM AUTHOR]

Requirements elicitation is one of the essential steps towards software design and construction. Business analysts and stakeholders often face challenges in gathering or conveying key software requirements. There are many methods and tools designed by researchers and practitioners but with the persistent development of new technologies, there is a need to make requirements gathering and design‐rationale process more efficient and adaptable. Storytelling is an emerging concept and researchers are witnessing its effectiveness in education, community building, information system, and requirement elicitation. Objectives of this study are to devise a method for requirements elicitation and improving design‐rationales using story‐based techniques and evaluate the effectiveness of the proposed activity. To answer the research objectives, the authors have conducted open‐ended interviews to get feedback on the proposed method; the authors have case requirement from a running project to map how this method can be useful; and performed empirical evaluation of the proposed card‐based activity. The estimated regression model, in our study, has shown that participants' perception about the simplicity/easiness and the joy of playing the game has an eventual positive effect on requirements elicitation through enhancing user's desire to play the game, which in turn increases the collaborative learning outcomes of the game. [ABSTRACT FROM AUTHOR]

Uncertainty and imprecision play an important role in the specification and analysis of complex systems. Therefore, it is important to provide methodologies and tools to support the correct development of these systems. In this paper we present a new formalism, based on fuzzy automata, to facilitate the different phases involved in the development of a system where information is fuzzy. The formal syntax and semantics of our formalism are based on previous work, which has been adapted to be easily implemented and automated. We introduce a methodology to analyze systems modelled with one of our fuzzy automata. Finally, we show how our framework can be used to define a model of the heart based on electrocardiograms (ECGs) and use this model to analyze data of real patients. [ABSTRACT FROM AUTHOR]

In automobile industry, it is a common approach to develop automobile real-time operating systems under some standards. For instance, OSEK/VDX is a world-wide adopted open standard. Traditional workflow is to first understand the standard, design and develop a system, then test its conformance to the standard, and finally deploy. There are several issues with the traditional workflow, e.g., ambiguities in standards may lead to incorrect design and implementation of real-world systems; the conformance of real-world systems to standards is difficult to check; and bug fixing after implementation is costly. To remedy the situation, in this paper, we present a unified executable formal automobile kernel under OSEK/VDX standard by defining the operational semantics of the system services in the standard using a rewrite-based executable semantic framework called $\mathbb {K}$. The formal kernel is unified in that it serves multiple purposes such as: 1) formal modeling of the OSEK/VDX standard helps detect ambiguities in the standard; 2) the executable kernel is essentially a formal model of the standard, which can be used to verify the correctness of automobile applications; and 3) verified applications can be used as test cases to check the conformance of a real-world automobile operating system against the OSEK/VDX standard. Using the formal kernel, we identify several ambiguities in the OSEK/VDX standard and a potential deadlock vulnerability in an industrial automobile application. [ABSTRACT FROM AUTHOR]

UML diagrams are the conventional methods for visual modeling systems. Among them, the Statechart diagrams are used to show the runtime behavior of a system, but the correctness of such diagrams is the primary concern of the designers because of concurrency issues like livelock, inaccessible states, and non-deterministic states. Process algebra methods have the capabilities that are suitable for verification and validation of Statecharts. To this end, in this paper, process algebra language LOTOS (Language Of Temporal Ordering Specification) is used as the target language, and a method is presented to map UML Statecharts to the LOTOS processes, called USLP. Then the correctness of the proposed mappings is proved by demonstrating the isomorphism relation between the Labeled Transition System (LTS) of a Statechart and the LTS of its transformed LOTOS specification. Next, tools CADP (Construction and Analysis of Distributed Processes) is used for verification and validation of the mapped LOTOS models, and the CSP process algebra and its tools, FDR are used to verify the properties could not be verified by the LOTOS and its toolset. The experimental results show our approach can: (1) verify some properties (the issues) that are not verified by other approaches and (2) reduce the space that should be searched to verify the properties. • Verification and validation of UML Statecharts are needed due to issues like livelock, inaccessible states, and non-deterministic states. • Process algebra methods have the abilty to verify and validate UML Statecharts. • The LOTOS process algebra is used to map and verify and validate the Statecharts. • Tools CADP is used to apply LOTOS models. • The proposed approach is evaluated using two case studies. [ABSTRACT FROM AUTHOR]

Compliance with the new European General Data Protection Regulation (Regulation (EU) 2016/679, GDPR) and security assurance are currently two major challenges of Cloud‐based systems. GDPR compliance implies both privacy and security mechanisms definition, enforcement and control, including evidence collection. This study presents a novel DevOps framework aimed at supporting Cloud consumers in designing, deploying and operating (multi)Cloud systems that include the necessary privacy and security controls for ensuring transparency to end‐users, third parties in service provision (if any) and law enforcement authorities. The framework relies on the risk‐driven specification at design time of privacy and security level objectives in the system service level agreement and in their continuous monitoring and enforcement at runtime. [ABSTRACT FROM AUTHOR]

In this study, the requirements elicitation approach employed in the context of the KONFIDO project is presented. KONFIDO introduces a technical paradigm for secure and interoperable cross‐border health data exchange by leveraging novel approaches and cutting‐edge technologies, such as homomorphic encryption and blockchains. Being a key part of the overall user requirements engineering methodology, requirements elicitation focused on producing high‐level, end‐user goals following a systematic procedure. First, the main business processes were identified based on the project's pilot scenarios. These business processes were the subject of a threat analysis, which identified the respective assets and a list of security risks/threats. Threats were further elaborated, considering the outcome of relevant projects and applicable best practices/standards. As a result, a set of user goals were identified and analysed in detail. Finally, a meta‐analysis of the produced goals against the employed information sources was applied, highlighting the importance of standards as a guide for defining requirements, as well as the complexity concerning the interdependencies among the elaborated business processes, assets, threats, and user goals. As the deployment of the technical solution may be cloud‐based, implications and challenges imposed by the adoption of cloud computing in this setting are also presented. [ABSTRACT FROM AUTHOR]

Gamification is a research field that is intended to increase motivation, so it is especially indicated in human capital intensive environments such as the software industry. Within Software Engineering, one of the main issues regarding software process improvement (SPI) is personnel motivation in specific SPI initiatives. These issues are stronger in small and medium software development companies where employees have to deal with the pressure of deadlines and occasional work overload. To address the adoption of SPI initiatives, the researchers implemented a defined gamification framework for deployment in SPI efforts in order to increase motivation among software workers and to enhance SPI results. The framework was rolled out in a small Spanish software development organisation, which is conducting internal SPI initiatives. To validate the effectiveness of the implemented framework, a controlled experiment was carried out in which an experimental group adopted SPI improvements using a gamification approach. The implementation results show that the application of the framework does not increase personnel motivation in SPI tasks although it contributes to enhancing the SPI tasks performance. This study discusses the limitations and recommendations to implement appropriately the SPI‐gamification framework in the scope of small and medium software development companies. [ABSTRACT FROM AUTHOR]

In role-based access control (RBAC), users gain access to predetermined roles and permissions. Thus, desired results are not achieved in emergency situations through policy in RBAC. In emergency situations, users should sometimes gain access to resources not authorized in normal situations. To increase the flexibility of access control, Break the Glass (BTG) policy was proposed. It allows users to break or override access controls, while every operation is documented to create maximum responsibility for users. Users with BTG access have maximum freedom to override the access controls and constraints of the model. In this paper, the flexibility of RBAC is enhanced by proposing an Emergency RBAC (E-RBAC), which uses BTG policy for managing the system in emergency situation. However, separation of duty (SOD) constraint is included to control and limit user access in this situation. Then, an administrative model is proposed to manage large E-RBAC systems. An administrative model reduces excessive burden for an administrator in large E-RBAC systems. At the next stage, E-RBAC is illustrated with medical and drug-dispensation scenarios and is then implemented through Alloy (the first logic language) so as to analyze the validity of model specifications. [ABSTRACT FROM AUTHOR]

Software requirements are an essential stepping stone for engineering any software system that meets the needs of its stakeholders. User interface (UI) contextual help provides end users with much‐needed support for understanding how to use a software system. This article presents an approach for generating contextual help from software requirements, while maintaining the ability to provide human input on the generated help. Domain classes, use cases, and UI flow models embody information that is valuable for help generation and are thereby used by the proposed approach. Templates are also used to define how requirements are associated with their contextual help counterpart elements. The generated help is represented using an existing contextual help definition language called CHAINXML. The latter was extended to support templates and alternatives in order to make the help generation process more seamless and to reduce the repetition in the generated help. The usefulness (usability and utility) of the generated help was evaluated by conducting a study with end users. The results showed that the participants found the help to be highly useful and most of them chose to use this help when given the opportunity to do so in a real‐life case. [ABSTRACT FROM AUTHOR]

Cyber‐physical systems (CPSs) are characterized by a multitude of physical and software. Particularly time‐related properties are of paramount importance and they can impact the behaviour of these systems. Designing and verifying CPS while tackling time‐related and physical properties are very important steps in the CPS life cycle development. Indeed, it is necessary to capture and characterize the different features and their dependencies with time through expressive models. Then, these models must be verified to prove their correctness. Existing process modelling languages such as business process modelling notation (BPMN) has been widely used to model business processes. However, BPMN lacks several features for modelling rich CPS processes such as those related to time and physical properties. In this study, the authors propose a verification framework for collaborative time‐aware CPS processes. In this context, they propose to extend BPMN to support the various CPS concepts and properties. Based on this extension, they propose a consistency verification approach, which aims to verify that the time‐related and physical properties associated with each process do not give rise to conflicts. Finally, they propose a compatibility verification approach, which aims to verify that the set of involved CPS processes form consistent inter‐CPS processes. [ABSTRACT FROM AUTHOR]

Abstract Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He's Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs. Highlights • Angelic nondeterminism, as understood in refinement calculi, is considered in CSP. • The UTP framework enables the systematic study of angelic nondeterminism. • A multirelational model for angelic choice in CSP requires a complete lattice. • Process algebras may be endowed with angelic choices that avoid divergence. [ABSTRACT FROM AUTHOR]

Abstract We demonstrate that modal transition systems with variability constraints are equally expressive as featured transition systems, by defining a transformation of the latter into the former, a transformation of the former into the latter, and proving the soundness and completeness of both transformations. Modal transition systems and featured transition systems are widely recognised as fundamental behavioural models for software product lines and our results thus contribute to the expressiveness hierarchy of such basic models studied in other papers published in this journal. [ABSTRACT FROM AUTHOR]

Requirements elicitation is a critical activity that forms part of the requirements engineering process because it has to discover what the software must do through a solid understanding of the wishes and needs of the various stakeholders and to transform them into software requirements. However, in spite of its relevance, there are only a few systematic literature reviews that provide scientific evidence about the effectiveness of the techniques used to elicit software requirements. This study presents a systematic review of relevant literature on requirements elicitation techniques, from 1993 to 2015, by addressing two research questions: Which mature techniques are currently used for eliciting software requirements? and Which mature techniques improve the elicitation effectiveness? Prior literature assumes that such 'maturity' leads to a better‐quality understanding of stakeholders' desires and needs, and thus an increased likelihood that a resulting software will satisfy those requirements. This research paper found 140 studies to answer these questions. The findings describe which elicitation techniques are effective and in which situations they work best, taking into account the product which must be developed, the stakeholders' characteristics, the type of information obtained, among other factors. [ABSTRACT FROM AUTHOR]

Understanding the users' needs is important for designing an application that provides a good usage experience. One can use design thinking (DT) to help identify those needs. Persona is a technique used in DT to support the requirements elicitation by describing user profiles. Nevertheless, the persona descriptions created using a traditional template may include many details about the users that are not relevant to the application design. To overcome this limitation, the authors proposed the PATHY technique to guide software engineers in creating and describing more useful personas, i.e. personas with information that is more relevant to the application design. They conducted an experiment to compare PATHY to another persona‐based technique which uses a traditional template and also supports the representation of the application's requirements. In this study, they assessed which of the two techniques helps to generate descriptions of personas that are more focused on potential requirements to consider in the design of the application. In addition, they analysed the efficiency of the techniques and the participants' perception of use. The results showed that PATHY generated more relevant characteristics for the application design than the technique that follows the traditional description. The PATHY was also more efficient for creating personas. [ABSTRACT FROM AUTHOR]

The majority of flaws found in software originates in the system requirements specification stage. The use of domain‐specific languages has shown to be a valuable resource in this part of the process, since they help to establish communication standards, enable automation and bring productivity and quality gains, in spite of their limited vocabulary. This study proposes the implementation of language of use case to automate models (LUCAM), a domain‐specific language that allows specification of textual use cases and semi‐automated generation of use case diagrams, class diagrams and sequence diagrams through LUCAMTool. To verify the feasibility of the proposed solution, tests were performed in both simulated and real environments so as to comprise a variety of scenarios observed in systems development. The approach assists in the requirement analysis and modelling, minimising existing problems in natural language specification, such as the dependence on the knowledge of specialists, uncertainty, ambiguity and complexity. [ABSTRACT FROM AUTHOR]

Regression testing ensures that the functionality of previous code is not affected by the updates in the modified code. The focus of regression test case generation is to generate test cases for changed functionality. The authors' research advocates the use of mobile agent‐based technology for regression test case generation using syntax and semantics analysis based on model and formal specifications. In this study, the authors presented a tool for adopting multi‐agent systems for regression test case generation on distributed environment using standard unified modelling language (UML) models and formal specifications. Different agents are designed to perform model comparison, behaviour comparison, specifications comparison, impact analysis, and regression test case generation. Agents designed in JADE framework perform these tasks by using XML files of UML class diagram, sequence diagram and formal specifications based on Object‐Z and OCL. To the best of the authors' knowledge, no research has reported regression test case generation using mobile agent‐based technology along with model and formal specifications. It is found that the use of mobile agents will significantly reduce time and effort for regression test case generation in distributed systems. [ABSTRACT FROM AUTHOR]

Emergency response is a knowledge‐intensive process that is very hard to model and automate. This primarily returns to the unpredictability and unrepeatability nature that characterises such process. Traditional modelling approaches are too rigid and do not effectively support the flexibility and dynamicity required by emergency response process. Case Management Model and Notation (CMMN) is a new standard modelling specification that has recently been released by Object Management Group (OMG) to standardise the modelling of Case Management approach. The objective of this study is to demonstrate how the CMMN can be used to model emergency response process. The authors use the CMMN to build a template model for a generic emergency response process. This model can easily be extended or interchanged among different modelling tools or execution platforms. In addition, they present a case study of a flood management process as a concrete example of using CMMN in modelling emergency response process. Finally, they conclude that the CMMN has a great potential to model case‐based processes such as emergency response, but CMMN still in its infancy. As a result, there is a lack of mature modelling tools and execution engines to execute the CMMN models. [ABSTRACT FROM AUTHOR]

Requirements engineering is a social process and while working together, stakeholders develop socio‐technical relationships. Socio‐technical aspects such as communication (information exchange among members) and awareness (knowledge of others) were discussed in literature, but little is known with respect to their role in requirements engineering activities. Therefore, requirements‐driven collaboration (RDC), particularly on the relevance of socio‐technical aspects, warrants further investigation. The authors aim to fill this gap by conducting a systematic literature review on these two aspects. This review covers planning (defining objectives and search strategy), execution (study search and selection), and interpretation of the findings (results and discussions). Findings revealed more studies on communication than on awareness. Two aspects of communication covered for RDC in literature are: (i) preferred communication medium, and (ii) communication patterns of teams. However, for awareness the aspects affecting awareness and vice versa were studied for RDC. Further investigation indicated the interdependence of awareness and communication and that distance does not affect team's awareness. The authors discuss implications for software practitioners in terms of enhancing their performance by considering the role of information brokers, and identifying central and emergent members etc. Researchers can strengthen the domain by providing more empirical results on interdependence of socio‐technical aspects. [ABSTRACT FROM AUTHOR]

In a literature review on the last 20 years of automated analysis of feature models, the formalization of analysis operations was identified as the most relevant challenge in the field. This formalization could provide very valuable assets for tool developers such as a precise definition of the analysis operations and, what is more, a reference implementation, i.e., a trustworthy, not necessarily efficient implementation to compare different tools outputs. In this article, we present the FLAME framework as the result of facing this challenge. FLAME is a formal framework that can be used to formally specify not only feature models, but other variability modeling languages (VML s) as well. This reusability is achieved by its two-layered architecture. The abstract foundation layer is the bottom layer in which all VML-independent analysis operations and concepts are specified. On top of the foundation layer, a family of characteristic model layers-one for each VML to be formally specified-can be developed by redefining some abstract types and relations. The verification and validation of FLAME has followed a process in which formal verification has been performed traditionally by manual theorem proving, but validation has been performed by integrating our experience on metamorphic testing of variability analysis tools, something that has shown to be much more effective than manually designed test cases. To follow this automated, test-based validation approach, the specification of FLAME, written in Z, was translated into Prolog and 20,000 random tests were automatically generated and executed. Tests results helped to discover some inconsistencies not only in the formal specification, but also in the previous informal definitions of the analysis operations and in current analysis tools. After this process, the Prolog implementation of FLAME is being used as a reference implementation for some tool developers, some analysis operations have been formally specified for the first time with more generic semantics, and more VML s are being formally specified using FLAME. [ABSTRACT FROM AUTHOR]

Commonly, simulation by using an existing network simulation tool or a simulator developed from scratch is employed for validation of analytical network performance models. An analytical model of star-shaped wireless sensor networks has been proposed in the literature in which, upon receiving a query from the coordinator, each sensor node sends one data frame to it by executing the IEEE 802.15.4 unslotted carrier-sense multiple access with collision avoidance algorithm. The model consists of expressions for calculation of the probability of successful receipt of the data at a certain time and the like. The authors of the model have written a special simulation program in order to validate the expressions. Our aim was to employ probabilistic model checker PRISM instead. PRISM only requires the user to formally specify the network as a kind of state machine and the queries about the probabilities sought in the form of logical formulas. It finds the probabilities automatically and can present them on graphs. We show how to specify the networks formally in such a way that all the expressions from the analytical model can be validated with PRISM. For those networks containing a few nodes, the validation can be carried out by normal model checking, which, in contrast to the simulation, always checks all the possible network behaviors, whereas statistical model checking can be used for the larger networks. [ABSTRACT FROM AUTHOR]

A cyber-physical system (CPS) is an integration of computation with physical processes whose behavior is defined by both computational and physical parts of the system. In this paper, we present a view of the challenges and opportunities for design automation of CPS. We identify a combination of characteristics that define the challenges unique to the design automation of CPS. We then present selected promising advances in depth, focusing on four foundational directions: combining model-based and data-driven design methods; design for human-in-the-loop systems; component-based design with contracts, and design for security and privacy. These directions are illustrated with examples from two application domains: smart energy systems and next-generation automotive systems. [ABSTRACT FROM AUTHOR]

Different modelling approaches have been proposed to automate the process of design and development of data warehouse. Some of them use the model driven architecture, however they are more focused on designing platform independent model (PIM) and platform specific model (PSM) and reserved unfortunately few efforts for requirements modelling and design computational independent model (CIM). This situation can be explained essentially by the presence of mature technologies and methods used for the representation of PIM and PSM models. Moreover, there are no standards to build CIM. Within this context, data warehousing projects fail due to not much attention paid on the requirement analysis phase. To overcome this problem, this study provides an approach to build a CIM architecture for modelling data warehouse requirements using an unified modelling language (UML) profile that extends the use cases and business process models, and proposes requirements specifications using SBVR structured English. [ABSTRACT FROM AUTHOR]

We present two data-aware algorithms to automatically derive web service compositions from global specifications. We show that a natural projection oriented derivation does not work in general, since some issues arise when projecting the set of implementations from the global specification, and we show how our approach deals with them. We use the constructions of two well-known languages as basis to define our models. In particular, given a WS-CDL choreography, our algorithms automatically extract a set of WS-BPEL compliant processes such that the interaction among these processes reproduces the behavior depicted in the choreography. This is achieved by introducing some control messages which make services coordinate as expected. With respect to our previous work on this kind of derivations, the main improvement of the models and derivations given in this work is their data-awareness , that is, the introduction of variables within the model, which strongly improves the expressiveness of our previous model based on FSMs. As a result, the formal model is enriched with new constructions such as workunits, which enable the definition of a complex conditional behaviour, and the derivation algorithms are necessarily more complex and sophisticated. The new derivation algorithms are implemented in the new version of our public derivation tool DIEGO. [ABSTRACT FROM AUTHOR]

We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems from informal requirements. Various views of a system, modeled as requirement interfaces, are naturally combined by conjunction. We develop an incremental test generation procedure with several advantages. The test generation is driven by a single requirement interface at a time. It follows that each test assesses a specific aspect or feature of the system, specified by its associated requirement interface. Since we do not explicitly compute the conjunction of all requirement interfaces of the system, we avoid state space explosion while generating tests. However, we incrementally complete a test for a specific feature with the constraints defined by other requirement interfaces. This allows catching violations of any other requirement during test execution, and not only of the one used to generate the test. This framework defines a natural association between informal requirements, their formal specifications, and the generated tests, thus facilitating traceability. Finally, we introduce a fault-based test-case generation technique, called model-based mutation testing, to requirement interfaces. It generates a test suite that covers a set of fault models, guaranteeing the detection of any corresponding faults in deterministic systems under test. We implemented a prototype test generation tool and demonstrate its applicability in two industrial use cases. [ABSTRACT FROM AUTHOR]

In order to provide a rigorous foundation for Software Product Lines (SPLs), several fundamental approaches have been proposed to their formal behavioral modeling. In this paper, we provide a structured overview of those formalisms based on labeled transition systems and compare their expressiveness in terms of the set of products they can specify. Moreover, we define the notion of tests for each of these formalisms and show that our notions of testing precisely capture product derivation, i.e., all valid products will pass the set of test cases of the product line and each invalid product fails at least one test case of the product line. [ABSTRACT FROM AUTHOR]

The class diagram is a tool for developing object-oriented software. It is essential that its interpretation by any analyst lacks ambiguity. In this paper, we present an interpretation of the class diagram from the perspective of an equational logic through a systematic breakdown of each of its elements. Our aim is to provide a formal specification for the class diagram susceptible of being processed and executed. For our formalization, we used the Maude language, because it allows us to define formal algebraic specifications for abstract data types. [ABSTRACT FROM AUTHOR]