International Journal of Software Engineering and Knowledge Engineering

Petri nets, a formal model for concurrent and distributed systems, have been widely applied in system modeling and analysis in almost every branch of computer science and many other scientific and engineering disciplines in the past half century. In this comprehensive survey, we review some major developments of Petri nets that have enhanced their modeling capabilities and in particular the methods to incorporate well-known software engineering development paradigms in Petri nets to support general software system modeling.

Cloud computing allows for access to ubiquitous data storage and powerful computing resources through the use of web services. There are major concerns, however, with data security, reliability, and availability in the cloud. In this paper, we address these concerns by introducing a novel security mechanism for secure and fault-tolerant cloud information storage. The information storage model follows the RAID (Redundant Array of Independent Disks) concept by considering cloud service providers as independent virtual disk drives. As such, the model utilizes multiple cloud service providers as a cloud cluster for information storage, and a service directory for management of the cloud clusters including service query, key management, and cluster restoration. Our approach not only supports maintaining the confidentiality of the stored data, but also ensures that the failure or compromise of an individual cloud provider in a cloud cluster will not result in a compromise of the overall data set. To ensure a correct design, we present a formal model of the security mechanism using hierarchical colored Petri nets (HCPN), and verify some key properties of the model using model checking techniques.

Dealing with crosscutting concerns has been a critical problem in software development processes. To facilitate handling crosscutting concerns at design phases, we proposed an aspect-oriented modeling and integration approach with UML activity diagrams. The primary concerns are depicted with UML activity diagrams as primary models, whereas crosscutting concerns are described with aspectual extended activity diagrams as aspect models. Aspect models can be integrated into primary models automatically. The AOM approach can reduce the complexity of design models. However, potential faults that violate desired properties of the software system might still be introduced during the modeling or integration processes. The verification technique is well-known for its ability to assure the correctness of models and uncover design problems before implementation. We propose a framework to verify aspect-oriented UML activity diagrams based on Petri net verification techniques. For verification purpose, we transform the integrated activity diagrams into Petri nets and prove the consistency of the transformation. Then, crosscutting concerns in system requirements are refined to properties in the form of CTL formulas. Finally, the Petri nets are verified against the formalized properties to report whether the aspect-oriented design models satisfies the requirements. Furthermore, we implement a tool named Jasmine-AOV to support the verification process. Case studies are conducted to evaluate the effectiveness of the proposed approach.

Petri nets are a powerful formalism in modeling workflows. A workflow determines the flow of work according to pre-defined business process. In many situations, business processes are constrained by scarce resources. The lack of resources can cause contention, the need for some tasks to wait for others to complete, which slows down the accomplishment of larger goals. In our previous work, a resource-constrained workflow model was introduced and a resource requirement analysis approach was developed for emergency response workflows, in which support of on-the-fly workflow change is critical [14]. In this paper, we propose a Petri net based approach for recourse requirements analysis, which can be used for more general purposes. The concept of resource-oriented workflow nets (ROWN) is introduced and the transition firing rules of ROWN are presented. Resource requirements for general workflows can be done through reachability analysis. An efficient resource analysis algorithm is developed for a class of well-structured workflows, in which when a task execution is started it is guaranteed to finish successfully. For a task that may fail in the middle of execution, an equivalent non-failing task model in terms of resource consumption is developed.

Goal-oriented requirements analysis (GORA) is one of the promising techniques to elicit software requirements, and it is natural to consider its application to security requirements analysis. In this paper, we proposed a method for goal-oriented security requirements analysis using security knowledge which is derived from several security targets (STs) compliant to Common Criteria (CC, ISO/IEC 15408). We call such knowledge security ontology for an application domain (SOAD). Three aspects of security such as confidentiality, integrity and availability are included in the scope of our method because the CC addresses these three aspects. We extract security-related concepts such as assets, threats, countermeasures and their relationships from STs, and utilize these concepts and relationships for security goal elicitation and refinement in GORA. The usage of certificated STs as knowledge source allows us to reuse efficiently security-related concepts of higher quality. To realize our proposed method as a supporting tool, we use an existing method GOORE (goal-oriented and ontology-driven requirements elicitation method) combining with SOAD. In GOORE, terms and their relationships in a domain ontology play an important role of semantic processing such as goal refinement and conflict identification. SOAD is defined based on concepts in STs. In contrast with other goal-oriented security requirements methods, the knowledge derived from actual STs contributes to eliciting security requirements in our method. In addition, the relationships among the assets, threats, objectives and security functional requirements can be directly reused for the refinement of security goals. We show an illustrative example to show the usefulness of our method and evaluate the method in comparison with other goal-oriented security requirements analysis methods.

Coverage-based fault localization techniques leverage the coverage information to identify the faulty elements of a program. However, these techniques can be adversely affected by coincidental correctness, which occurs when the defect is executed but no failure is revealed. In this paper, we propose a clustering-based strategy to identify coincidental correctness in fault localization. The insight behind this strategy is that tests in the same cluster have similar behaviors. Thus a passed test in a cluster with many failed tests is highly possible to be coincidentally correct because it has the potential to execute the faulty elements as those failed ones do. We evaluated this technique from two aspects: the ability to identify coincidental correctness and the effectiveness to improve fault localization. The experimental results show that our strategy can alleviate the coincidental correctness problem and improve the effectiveness of fault localization.