Quadrotors are popular small unmanned aerial vehicles (UAVs) deployed in many real-world applications such as aerial surveying. Despite their simple mechanical construction and propulsion principle, quadrotors have nonlinear dynamics and require advanced stabilizing control. This paper presents an approach combining deep learning, control theory, and convex optimization to design neural net controllers to stabilize quadrotors, which provides the basis for developing neural net controllers to stabilize more sophisticated drones.

Cyber-physical systems (CPS) have become increasingly important in the functioning of our society.In recent years, machine learning (ML) approaches start to become an attractive choice to design CPS controllers for better performance and adaptability.How to assure the correctness of this type of new controllers is extremely difficulty and remains a grand research challenge.This paper presents a convex optimization-based technique for computing the stability regions of deep neural net (DNN) controllers for CPS.The technique has been successfully applied to three benchmark systems.

Cyber-physical systems (CPS) have become increasingly important in the functioning of our society. In recent years, machine learning (ML) approaches have started to become an attractive choice to design CPS controllers for better performance and adaptability. Assuring the correctness of this type of controller is extremely difficulty and remains a grand research challenge. Stability is a critical correctness property of any CPS. Designing stable conventional controllers for linear system dynamics is well-understood based on the control theory from the past half century. Designing stable deep neural net (DNN) controllers for linear system dynamics is new while designing stable DNN controllers for non-linear system dynamics is a major research challenge. Although demonstrating the stability of a controller using simulation is a widely accepted practice, this approach does not provide required assurance for CPS involved in safety and mission-critical applications. A provable stability region of attraction (RoA) provides a strong assurance guarantee. In this paper, we have developed an approach to build and verify stable DNN controllers for nonlinear systems, which includes using deep reinforcement learning to design and train a DNN controller based on nonlinear system dynamics, approximating the non-linear system dynamics with several well-known linearization techniques, and leveraging a recent method in deriving the RoA on linearized system dynamics. We have applied this approach to one well-known benchmark system with non-linear dynamics and have obtained their approximated stability RoAs based on several linearization techniques.

Cyber-physical systems (CPSs) with controllers built using deep neural nets and reinforcement learning (DRL) have become increasingly used in the functioning of our society. How to assure the correctness such as the safety and stability of these DNN controllers is extremely important and remains a major research challenge. This paper presents an approach to build safe and stable DNN controllers using DRL and deep imitation learning (DIL). An initial DNN controller is built using DRL, which is used to bootstrap a behavior preserving target DNN controller with safety and stability guarantees via DIL. We have applied this approach in successfully building safe and stable DNN controllers of a simplified airplane pitch control system.

Cyber-physical systems (CPSs) are ubiquitous and are becoming increasingly important in the functioning of our society.CPSs have complex discrete and continuous behaviors.In recent years, learning enabled components (LECs) built using machine learning approaches are increasingly used in CPSs to perform autonomous tasks to deal with uncertain and unfamiliar environments.CPSs with LECs are even more difficult to develop.We have developed a methodology for formally modeling and analyzing CPSs with LECs.Hybrid predicate transition nets (HPrTNs) are used as the underlying formal method to model CPSs with LECs and their training through their simulation capability.In this paper, we present our new analysis methodology for CPSs with LECs consisting of three complementary techniques, including a testing technique based on HPrTN simulation capability, a simulation guided barrier certificate technique, and a SMT based bounded model checking technique.The above analysis methodology is partially supported by a tool chain and is demonstrated through an example.

Cyber-physical systems are complex systems with hybrid behaviors. In this paper, hybrid predicate transition nets (HPrTNs) are proposed for modeling and analyzing cyberphysical systems. HPrTNs are formally defined and their relationships to hybrid automata are shown. Important features of HPrTNs including continuous places, differential equations for defining token evolution, and net composition are discussed. The applicability of HPrTNs is demonstrated through several wellknown benchmark hybrid systems.

As the most common non-deadlock concurrency bugs, atomicity violations are extremely hard to detect during testing since the exhaustive testing of a multi-threaded program is impossible because of the large number of interleavings. The studies in recent years have mainly focused on single-variable atomicity violation. However, those methods are unable to predict or find atomicity violations with multiple variables involved. Many variables are inherently correlated and need to be accessed together with their correlated peers in a consistent manner. These variables need to be either updated together consistently or accessed together to avoid inconsistent update or reading. This paper presents a method for predicting two-variable atomicity violation, based on access correlation between variables and atomicity violation pattern of variable accesses, including algorithms to infer access correlation between variables and to predict atomicity violation using model checking. The effectiveness of our method is evaluated with several real-world systems.

Hybrid systems, especially in the form of cyber physical systems, have become ubiquitous and are playing critical roles in the functioning of society, however their design and implementation are extremely difficulty, especially regarding their dependability.In this paper, we propose a hybrid high level Petri net formalism, hybrid predicate transition nets (HPrTNs), for modeling and analyzing hybrid systems.We discuss some critical concepts and features of HPrTNs.We demonstrate the applicability of HPrTNs through several well-known benchmark hybrid systems and compare our results with other relevant methods.HPrTNs are fully supported in the tool environment PIPE+.

Cyber physical systems (CPSs) are pervasive in our daily life from mobile phones to auto driving cars.CPSs are inherently complex due to their sophisticated behaviors and thus difficult to build.In this paper, we propose a systematic approach to develop CPSs with quality assurance throughout the development process.A CPS is abstracted and partitioned into a set of independent executing agents, where each agent is further refined into a set of behaviors.Each behavior is modeled with a high level Petri net, called behavior net.The overall behavior of an agent is modeled by an agent through composing individual behavior nets.Finally, the overall system behavior is modeled by a system net through integrating individual agent nets incrementally.Simulation and model checking can be performed on individual behavior nets, agent nets, and the final system net.The resulting system net is systematically mapped to behavior programs in Java, which are enhanced and extended with domain specific functionality.A set of property patterns based on behavior program is developed, which are used to generate runtime monitors to check behavior program executions.We demonstrate our approach using a multi-car parking system.

Android permission framework is a part of Android OS to enforce secure cross application communication. However the Android permission framework is very complex, and its descriptions are scattered in dozens of webpages. It is very difficult to understand the relationships among multiple permission levels and their potential vulnerabilities. This paper presents a formal model of the Android permission framework using high level Petri nets. The model precisely defines the complex relationships among different levels of permissions. The model is constructed incrementally and thus is easily adaptable to future changes. The model building process is supported by our tool environment PIPE+, which further provides several analysis techniques. Simulation results for several scenarios that obey and violate the permission requirements are discussed.

High level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains.However, their strong expressive power hinds their analyzability.In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs -predicate transition (PrT) nets.This method extends and improves our prior results by covering more PrT net features including full first order logic formulas and exploring additional alternative translation schemes.This new analysis method is supported by a tool chain -front end PIPE+ for creating and simulating PrT nets and back end SPIN for model checking safety and liveness properties.We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015.We discuss several properties and show the detailed model checking results of two properties in one system.

Cyber physical systems (CPSs) are pervasive in our daily life from mobile phones to auto driving cars.CPSs are inherently complex due to their sophisticated behaviors and thus difficult to build.In this paper, we propose a framework to develop CPSs based on a model driven approach with quality assurance throughout the development process.An agent-oriented approach is used to model individual physical and computation processes using high level Petri nets, and an aspect-oriented approach is used to integrate individual models.The Petri net models are systematically mapped to classes and threads in Java, which are enhanced and extended with domain specific functionalities.Complementary quality assurance techniques are applied throughout system development and deployment, including simulation and model checking of design models, model checking of Java code, and run-time verification of Java executable.We demonstrate our framework using a car parking system.

High-level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains. However, their strong expressive power hinders their analyzability. In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs — predicate transition (PrT) nets. This method extends and improves our prior results by covering more PrT net features including full first-order logic formulas and exploring additional alternative translation schemes. This new analysis method is supported by a tool chain — front-end PIPE[Formula: see text] for creating and simulating PrT nets and back-end SPIN for model checking safety and liveness properties. We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015. We discuss several properties and show the detailed model checking results in one system.

Cyber-physical systems (CPSs) are pervasive in our daily life from mobile phones to auto-driving cars. CPSs are inherently complex due to their sophisticated behaviors and thus difficult to build. In this paper, we propose a framework to develop CPSs based on a model-driven approach with quality assurance throughout the development process. An agent-oriented approach is used to model individual physical and computation processes using high-level Petri nets, and an aspect-oriented approach is used to integrate individual models. The Petri net models are systematically mapped to classes and threads in Java, which are enhanced and extended with domain-specific functionalities. Complementary quality assurance techniques are applied throughout system development and deployment, including simulation and model checking of design models, model checking of Java code, and runtime verification of Java executable. We demonstrate our framework using a car parking system.

Security has become an essential and critical nonfunctional requirement of modern software systems, especially cyber physical systems.Security patterns aim at capturing security expertise in the worked solutions to recurring security design problems.This paper presents an approach to formally model and analyze six security patterns to detect potential incompleteness, inconsistency, and ambiguity in the textual descriptions; and to prevent their incorrect implementation.These patterns are modeled using high level Petri nets in our tool environment PIPE+.Simulation is used to analyze various security relevant properties.The validated formal models of individual security patterns serve as the building blocks for system design involving the composition of multiple security patterns.

High level Petri nets (HLPNs) have been widely applied to model concurrent and distributed systems in computer science and many other engineering disciplines. However, due to the expressive power of HLPNs, they are difficult to analyze. In recent years, a variety of new analysis techniques based on model checking have been proposed to analyze high level Petri nets in addition to the traditional analysis techniques such as simulation and reachability (coverability) tree. These new analysis techniques include (1) developing tailored model checkers for particular types of HLPNs or (2) leveraging existing general model checkers through model translation where a HLPN is transformed into an equivalent form suitable for the target model checker. In this paper, we present a term rewriting approach to analyze a particular type of HLPNs -- predicate transition nets (PrT nets). Our approach is completely automatic and implemented in our tool environment, where the frontend is PIPE+, a general graphical editor for creating PrT net models, and the backend is Maude, a well-known term rewriting system. We have applied our approach to the Mondex system -- the 1st pilot project of verified software repository in the worldwide software verification grand challenge, and several well-known problems used in the annual model checking contest of Petri net tools. Our initial experimental results are encouraging and demonstrate the usefulness of the approach.

High level Petri nets (HLPNs) have been widely used to model complex systems; however, their high expressive power costs their analyzability.Model checking techniques have been exploited in analyzing high level Petri nets, but have limited success due to either undecidability problem or state explosion problem.Bounded model checking (BMC) is a promising analysis method that explores state space within a predefined bound.BMC sacrifices the completeness of traditional model checking but becomes more practical and often effective to analyze large models.In our prior work, we have developed a method based on BMC and a supporting tool PIPE+Verifier to analyze high level Petri nets using a state of the art satisfiability modulo theories (SMT) solver Z3 as the backend engine.Our experiment results have been very encouraging.In this paper, we present the design, implementation, and use of PIPE+Verifier, as well as show additional improvements to make PIPE+Verifier more efficient.

This paper presents a methodology for analyzing multi-agent systems modeled in nested predicate transition nets. The objective is to automate the model analysis for complex systems, and provide a foundation for tool development. We formally define the translation rules that translate the multi-agent model to an executable PROMELA model, and demonstrate the translation with an example.

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.

In the past two decades, multi-agent systems have emerged as a new paradigm for conceptualizing large and complex distributed software systems. Even though there are many conceptual frameworks for using multi-agent systems, there is no well established and widely accepted method for the representation of multi-agent systems. We adapt a well-known formal model, predicate transition nets, to include the notions of dynamic structure, agent communication and coordination to address the representation problems. This paper presents a comprehensive methodology for modeling multi-agents based on the extensions. We demonstrate our modeling approach with an example. Several case studies on different application domains from our previous works are also discussed.

Scientific workflows have recently emerged as a new paradigm for representing and managing complex distributed scientific computations and are used to accelerate the pace of scientific discovery. In many disciplines, individual workflows are large and complicated due to the large quantities of data used. As such, the workflow construction is difficult or even impossible when relevant domain knowledge is missing or the workflows require collaboration within multiple domains. Recent efforts from scientific workflow community aiming at large-scale capturing of provenance present a new opportunity for using provenance to provide recommendations during building scientific workflows. This paper presents a method based on provenance to mine models for scientific workflows, including data and control dependency. The mining result can either suggest part of others' workflows for consideration, or make familiar part of workflow easily accessible, thus provide recommendation support for scientific workflow composition.

A mobile agent system is a special distributed system with moving programs in networks. Mobile agent systems provide a powerful and flexible paradigm for building high performance distributed systems. Due to dynamic configuration property, assuring quality of a mobile agent system is a challenge work. Formal specification and analysis of a mobile agent system provides one of the best approaches to ensure the correctness of a system design. However, it is difficult to find a formal specification tool for modeling a mobile agent system with an easy to understand and concise model. In addition, it is a challenge but also important work to provide an automatic formal analysis approach for verifying whether a system specification correctly meets certain requirements in a mobile agent system. In this paper, a framework for specification and analysis of mobile agent systems is defined. First, Predicate/Transition nets are extended with dynamic channels for modeling mobile agent systems. The formalism has the expressive power to naturally model the software architecture of a mobile agent system, and easily capture the properties especially the mobility, mobile communication and dynamic configuration of a mobile agent system. Then, model checking is instrumented to the framework for automatically verifying the correctness of the specification of a mobile agent system. In order to illustrate the capability of the formalism and the verification strategy, a medical image processing system using mobile agents is modeled using the extended Predicate/Transition nets and system properties are verified using the SPIN model checker.

A software architecture design has many benefits including aiding comprehension, supporting early analysis, and providing guidance for subsequent development activities. An additional major benefit is if a partial prototype implementation can be automatically generated from a given software architecture design. However, in the past decade less progress was made on automatically realizing software architecture designs. In this paper, we present a translator for automatically generating an implementation from a software architectural description. The implementation not only captures the functionality of the given architecture description, but also contains additional monitoring code for ensuring desirable behavior properties through runtime verification. Our method takes a software description written in SAM, a software architecture model integrating dual formal methods Petri nets and temporal logic, and generates ArchJava/Java/AspectJ code. More specifically, the structure of a SAM architecture description produces ArchJava code, the behavior models of components/connectors represented in Petri nets lead to plain Java code, and the property specifications defined in temporal logic generate AspectJ code; the above code segments are then integrated into Java code. An experimental result is provided.

Current service architecture description language and composition approaches consider simplistic method invocation. They pay less attention to the formal semantics and verification of service composition in the design, and less support property specifications and architecture validation. This paper presents an executable web service architecture model, Service-Oriented Software Architecture Model (SO-SAM), which is an extension of SAM (Software Architecture Model [16]) to the web service applications, and verificationof web system properties in the design. SO-SAM describes each web service in terms of component and service composition in terms of connector separately. Furthermore, we validate SO-SAM model to prove that it facilitates the verification and monitoring of web services integration through translation to the Maude programming langauge, a high level language and high performance executable specification with the componentized and object-oriented design, as well as using model checking technique in the system design level. Finally, a case study of the validation of the model is demonstrated.

Software architectures shift developers' focus from lines-of-code to coarser-grained architectural elements and their interconnection structure. However, the benefits of architecture description languages (ADLs) cannot be fully captured without an automated realization of software architecture designs because manually shifting from a model to its implementation is error-prone. We propose an integrated approach for automatically translating software architecture design models to an implementation and validating the translation as well as the implementation by exploring runtime verification technique and aspect-oriented programming. Specifically, system properties are not only verified against design models, but also verified during the execution of the generated implementation of software architecture design. A prototype tool, SAM Parser, is developed to demonstrate the approach on SAM (Software Architecture Model). In SAM Parser, all the realization and verification code can be automatically generated without human intervention. In this paper, we first brief describe the approach report on a case study conducted at an e-commerce scenario, an online shopping system to assess the benefits of automated realization of software architecture design and validation in a Web service domain.

Security design at architecture level is critical to achieve high assurance software systems. However, most security design techniques for software architectures were in ad hoc fashion and fell short in precise notations. This paper proposes a formal aspect-oriented approach to designing secure software architectures. The underlying formalism is the software architecture model (SAM) that combines Petri nets and temporal logic. SAM supports a precise way to model the problem domain, its software architecture, and security aspects of the software architecture. An integrated architecture is obtained by weaving aspect models with the base architecture model. Mechanisms in SAM are amenable to analyzing correctness of the architecture design.

Mobile agents provide a powerful and flexible paradigm for the development of autonomic computing systems. However, due to the security concern, mobile agents are not popularly used for real-world systems. In this paper, we define a security framework that can effectively protect mobile agents and agent systems from intruder attacking. In the framework, a mobile agent finder, which is extended with a registration protocol, is used to authenticate and authorize agent systems, incoming messages, and agents. We formally model the secure mobile agent finder using predicate transition nets, and analyze the models using model checking tool Spin. The results help us to develop high confidence applications using mobile agents. In addition, the modeling and analysis approach can be easily extended to develop other complex software systems.

System assembly is one of the major issues in engineering complex component-based systems. This is especially true when heterogeneous, COTS and GOTS distributed systems, typical in industrial applications, are involved. The goal of system assembly is not only to make constituent components work together, but also to ensure that the components as a whole behave consistently and guarantee certain end-to-end properties. Despite recent advances, there is a lack of understanding about software composability, as well as theory and techniques for checking and verifying component-based systems. A theory of software system constraints about components, their environment and about system as a whole is the necessary foundation toward solid understanding of the composability of component-based systems. In this paper, we present a systematic approach for constraint specification and constraint propagation in concert with design refinement with a novel technique to ensure consistency between system-wide and component constraints in a design composition process of component-based systems. The consistent constraint propagation is used in our approach to drive progressive verification of the design. It allows us to verify overall design composition without interference of internal details of component designs. Verification is done separately at architectural and component levels without having to compose results of component analyses. A component can be safely replaced with alternative design without re-verifying the overall system composition so long as the replacement conforms to the corresponding interface and component constraint(s).

Non-functional properties reflect the quality of a software system and are essential for a successful software system, but analysis of non-functional properties is less well studied compared to that of functional properties. Performance, dependability and performability are most concerned non-functional properties in lifecritical systems. In this paper, a methodology is proposed to analyze dependability and performability using a modeling and analyzing framework called SAM. By incorporating stochastic information into a SAM model, dependability and performability as well as functional properties can be analyzed at software architecture level using proper analysis techniques under the uniform SAM framework.

The software architecture model (SAM) is a general software architecture model based on a dual formalism combining Petri nets and temporal logic. A SAM model contains a hierarchical set of compositions, each of which consists of a set of components, a set of connectors, and a set of constraints. This paper proposes a formal method for analyzing SAM models in both element (either component or connector) level and composition level. The basic idea is to simulate Petri net behaviors in terms of fair transition systems. The properties of individual components and connectors are verified either by deductive reasoning or model checking. The properties of the entire system is inferred from the properties of its constituents. A detailed case study of an electronic commerce system shows our approach to formally modeling, refining and analyzing software architecture models.

In the past decade, software architecture research has mainly focused on the concept formulation and the development of various architecture description languages. This field has matured enough and thus requires more emphasis on validation techniques. Symbolic model checking has been a highly successful automatic validation technique for hardware systems. We are interested in whether symbolic model checking can be effectively applied to software architecture validation. In this paper, we present our approach to apply the symbolic model checking technique to verify software architecture specifications written in SAM.

In the past decade, software architecture research has mainly focused on the concept formulation and the development of various architecture description languages. This field has now matured enough and thus requires more emphasis on techniques for developing and analyzing software architecture specifications. SAM is a general software architecture model for developing and analyzing software architectures. In this paper, we show how to integrate high-level Petri nets and first-order temporal logic as the foundation of SAM to establish a unified framework for specifying and analyzing all aspects of a software architecture. We provide a set of heuristics, which are supported by well-defined existing methods and techniques developed by other researchers as well as our own, for software architecture development and analysis. We demonstrate the application of this framework and the heuristics with an example.

Integration testing plays a crucial role in component-based software development. Complementary to the existing works on the selection of test cases and measurement of test adequacy in integration testing, the paper focuses on questions about how to observe the behaviours of a large and complicated system during dynamic testing. We first analyse the structure of white-box integration testing and propose a family of integration testing methods. We then discuss and formalise the requirements of proper uses of test drivers and component stubs in incremental integration. Finally, we propose a set of axioms for integration testing of concurrent systems.

Unified Modeling Language (UML) has been widely accepted as the standard object-oriented development methodology in the software industry. However, many graphical notations in UML only have informal English definitions and thus are error-prone and cannot be formally analyzed. We present our preliminary results on an approach to formally define UML class diagrams using hierarchical predicate transition nets (HPrTNs). We show how to define the main concepts related to class diagrams using HPrTN elements.

Software architecture has become one of the most active research topics in software engineering in recent years. One of the distinct features of software architecture research is to explicitly study the interconnections (connectors) among system components. In this paper, we show how to formally specify several well-known general connectors in a software architecture methodology called SAM. Related work is discussed and compared. Our results establish the basis for reusing these defined connectors and for building more sophisticated connectors from them.

Most legacy software systems were developed in imperative languages with traditional design approaches. Instead of continually maintaining these legacy systems in their original architecture and design at high cost, reengineering them to new systems with good design and architecture can significantly improve their understandability, reusability and maintainability. Design patterns (DPs) combine successful established design practices and experts' experiences into a set of inter-related components that exhibit known behaviours with better flexible structures. Software development with DPs provides easier understanding and standardization that make system evolution much more effective. In this paper, we use a parallel program generation environment (PPGE) as a case study to demonstrate the reengineering of a traditional software system into a pattern-based software system. An architecture using the dynamic-packing component library (ADPCL) composed of existing well-known design patterns, and a pattern-based reengineering approach for the transformation of systems are proposed. Copyright © 2000 John Wiley & Sons, Ltd.

Software reuse has the potential to improve software quality and productivity. Software reuse covers the whole process of identification, representation, retrieval, adaptation and integration of reusable software components. Although object-oriented software has potentially high reusability, retrieving reusable object-oriented software may be difficult when the reuse library is large and inaccessibly represented. Furthermore, it is hard to check the consistency of component integration due to the lack of formal descriptions of required components. In this paper, we propose a formal approach for component retrieval and integration analysis during the reuse process. During the reuse process, software components are specified with logical predicates. A two-layer specification method is proposed. The class-layer specification is used for component retrieval and the member function-layer specification is used for consistency analysis during component integration. A formal model, predicate transition nets, is used for dynamic integration analysis. We show how to derive predicate transition nets from individual components and integrated components, and how to detect potential inconsistencies by checking the reachability tree of the predicate transition net representing an integrated program. Based on the approach proposed in this paper, a comprehensive tool can be implemented. Copyright © 2000 John Wiley & Sons, Ltd.

Most of the legacy software systems were developed in imperative languages with traditional design approaches. Instead of continually maintaining these legacy systems at high cost, re-engineering them to new systems with good design and architecture can surely improve their understandability, reusability and maintainability. Design patterns (DPs) have integrated the concept of standardization and expert experiences into a set of inter-related components that can function certain behaviors with better flexible structure. The software development with DPs provides easier understanding and standardization that makes the system evolution much more effective. We use a parallel program generation environment (PPGE) as a case study to the re-engineering of a traditional software system into a pattern based software system. An architecture with the Dynamic-Packing Component Library (ADPCL) which is composed of existing well-known design patterns, and a pattern based re-engineering approach for transformation systems are also proposed.

In the past several years, various graphical techniques were proposed to analyze various types of structural errors, including inconsistency (conflict rules), incompleteness (missing rules), redundancy (redundant rules), and circularity (circular depending rules), of rule based systems. We present a special reachability graph technique based on /spl omega/-nets (a special type of low-level Petri net) to detect all of the above types of structural errors. Our new technique is simple, efficient, and can be easily automated. We highlight the unique features of this new approach and demonstrate its application through an example.

If software metrics are useful in a forward software engineering environment, they are vital in a reverse engineering environment. We are endeavouring to discover approaches to developing reverse engineering metrics for software engineers who need them for reverse engineering legacy systems. The major contribution of the paper is the presentation of a systematic research base and a hierarchical approach to the development of software metrics for reverse engineering. Measurement is fundamental to the software engineering discipline as a whole. A software metric is a quantitative measure of the degree to which a system, component, or process possesses a given attribute (N.E. Fenton and S.L. Pfleeger, 1996). Software reverse engineering is the process of analysing a subject system to: identify the system's components and their interrelationships; and create representations of the system at a higher level of abstraction (E.J. Chikofsky and J.H. Cross II, 1990). The goal of developing reverse engineering metrics is to identify measures that are needed for assessing the status of reverse engineering projects, products, processes and resources, and helping engineers to understand both what is happening and what will happen during reverse engineering procedures. Consequently, these concrete reverse engineering measures make more visible to us aspects of process and product in reverse engineering, in particular, the product of specifications and the process of abstractions and transformations. This makes it possible to control reverse engineering projects. Aspects of measurement in reverse engineering are outlined.

Design with reuse has been accepted as a cost-effective way to software development. Software reuse covers the process of identification, representation, retrieval, adaptation, and integration of reusable software components. In this paper, we propose a semi-formal approach to software reuse. The approach consists of the following major steps: (1) software components are annotated with formal information, (2) the software components are then translated into predicate transition nets, and (3) consistency checking of the reusable and new components is carried out using the reachability analysis technique of predicate transition (PrT) nets. The approach is demonstrated through an example.

A set of useful refinement rules on hierarchical predicate transition nets (HPrTNs in the sequel) is presented. These rules help a user to develop a large HPrTN in a stepwise approach supporting both top-down and bottom-up development styles. Furthermore, the author has shown that these rules either preserve or facilitate the verification of many system behavioral properties. Another nice feature of these rules is that their applications always result in a valid partial view and an extended and integrated definition of the original HPrTN. The author also briefly discusses related works on refinement techniques based on Petri nets and other specification methods.

The paper presents an approach to translate hierarchical predicate transition nets into CC++ (a concurrent object oriented language) program skeletons. The approach consists of an overall translation architecture and a set of translation rules based on the syntax and semantics of hierarchical predicate transition nets. The results have established a link between hierarchical predicate transition nets and concurrent object-oriented programming, and provided some building blocks for a hierarchical predicate transition net based transformational software development methodology.

Petri nets have been widely used as a tool for modeling and analyzing concurrent and distributed system for many years but their applications have been limited to the earlier activities of software system development. To make Petri nets a full fledged software development methodology, systematic (eventually automatic) code generation techniques are needed. We present an approach to derive parallel program skeletons from Petri nets which establishes a link between Petri nets and OO parallel programming and forms a foundation for a Petri net based transformational software development methodology.

Hierarchical high level Petri nets have been proposed in recent years as a powerful formal method for modeling large concurrent and distributed systems but they are even more difficult to analyze than flat high level Petri nets, which are also lacking effective analysis methods themselves. A method for analyzing properties of hierarchical predicate transition Petri nets is proposed. The method employs two temporal induction techniques, one for safety properties and the other for liveness properties, without using temporal logic formalism. Within each induction technique, a hybrid reasoning technique combining net structural and behavioral reasoning, and ordinary first order logic reasoning is used.

In previous work, a methodology for constructing hierarchical and structured high-level Petri net specifications has been developed. The authors further explore and refine the methodology for using hierarchical high-level Petri nets in systems analysis. The approach has adapted the results from the data flow diagram method and its application to modern systems analysis. The major steps and the associated techniques of the approach are presented and demonstrated through a library system.>

Abstract In this paper, a methodology for constructing hierarchical and structured predicate transition net specifications is developed, which includes new systematic notation extensions for supporting various transformation techniques upon predicate transition nets and several rules for applying such transformation techniques. The levelling technique in data‐flow diagrams is adapted in the refinement and the abstraction techniques, and the state decomposition idea in state‐charts is employed in designing various label formulation operators. The methodology is illustrated through the specification of a lift system. The methodology can significantly reduce the constructing complexity and enhance the comprehensibility of large predicate transition net specifications.

A new class of high-level Petri nets is defined, which is a combination of predicate transition nets and first order temporal logic. By combining these two formal methods, one can explicitly specify the structures and specify and verify various properties of parallel and distributed systems in the same framework, which cannot be achieved by using either one of the formal methods individually. Therefore, a more powerful methodology for the specification and the verification of parallel and distributed systems is obtained. The application of temporal predicate transition nets is illustrated through the specification and the verification of the five-dining-philosophers problem.>

Abstract This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.