Search

Expanding abbreviations in source code to their full meanings is very useful for software maintainers to comprehend the source code. The existing approaches, however, focus on expanding an abbreviation to a single word, i.e., unigram. They do not perform well when dealing with abbreviations of phrases that consist of multiple unigrams. This paper proposes a bigram-based approach for retrieving abbreviated phrases automatically. Key to this approach is a bigram-based inference model for choosing the best phrase from all candidates. It utilizes the statistical properties of unigrams and bigrams as prior knowledge and a bigram language model for estimating the likelihood of each candidate phrase of a given abbreviation. We have applied the bigram-based approach to 100 phrase abbreviations, randomly selected from eight open source projects. The experiment results show that it has correctly retrieved 78% of the abbreviations by using the unigram and bigram properties of a source code repository. This is 9% more accurate than the unigram-based approach and much better than other existing approaches. The bigram-based approach is also less biased towards specific phrase sizes than the unigram-based approach.

Unigram is a fundamental element of [Formula: see text]-gram in natural language processing. However, unigrams collected from a natural language corpus are unsuitable for solving problems in the domain of computer programming languages. In this paper, we analyze the properties of unigrams collected from an ultra-large source code repository. Specifically, we have collected 1.01 billion unigrams from 0.7 million open source projects hosted at GitHub.com. By analyzing these unigrams, we have discovered statistical properties regarding (1) how developers name variables, methods, and classes, and (2) how developers choose abbreviations. We describe a probabilistic model which relies on these properties for solving a well-known problem in source code analysis: how to expand a given abbreviation to its original indented word. Our empirical study shows that using the unigrams extracted from source code repository outperforms the using of the natural language corpus by 21% when solving the domain specific problems.

In high performance computing (HPC) resources’ extensive experiments are frequently executed. HPC resources (e.g. computing machines and switches) should be able to handle running several experiments in parallel. Typically HPC utilizes parallelization in programs, processing and data. The underlying network is seen as the only non-parallelized HPC component (i.e. no dynamic virtual slicing based on HPC jobs). In this scope we present an approach in this paper to utilize software defined networking (SDN) to parallelize HPC clusters among the different running experiments. We propose to accomplish this through two major components: A passive module (network mapper/remapper) to select for each experiment as soon as it starts the least busy resources in the network, and an SDN-HPC active load balancer to perform more complex and intelligent operations. Active load balancer can logically divide the network based on experiments’ host files. The goal is to reduce traffic to unnecessary hosts or ports. An HPC experiment should multicast, rather than broadcast to only cluster nodes that are used by the experiment. We use virtual tenant network modules in Opendaylight controller to create VLANs based on HPC experiments. In each HPC host, virtual interfaces are created to isolate traffic from the different experiments. The traffic between the different physical hosts that belong to the same experiment can be distinguished based on the VLAN ID assigned to each experiment. We evaluate the new approach using several HPC public benchmarks. Results show a significant enhancement in experiments’ performance especially when HPC cluster experiences running several heavy load experiments simultaneously. Results show also that this multi-casting approach can significantly reduce casting overhead that is caused by using a single cast for all resources in the HPC cluster. In comparison with InfiniBand networks that offer interconnect services with low latency and high bandwidth, HPC services based on SDN can provide two distinguished objectives that may not be possible with InfiniBand: The first objective is the integration of HPC with Ethernet enterprise networks and hence expanding HPC usage to much wider domains. The second objective is the ability to enable users and their applications to customize HPC services with different QoS requirements that fit the different needs of those applications and optimize the usage of HPC clusters.

With the increasing complexity of software, new access control methods have emerged to deal with attribute-based authorization. As a standard language for specifying attribute-based access control policies, XACML offers a number of rule and policy combining algorithms to meet different needs of policy composition. Due to their variety and complexity, however, it is not uncommon to apply combining algorithms incorrectly, which can lead to unauthorized access or denial of service. To solve this problem, this paper presents a fault-based testing approach for revealing incorrect combining algorithms in XACML 3.0 policies. The theoretical foundation of this approach relies on the formalization of semantic differences between rule combining algorithms and between policy combining algorithms. It allows the use of a constraint solver for generating queries to which a given policy produces different responses than its combining algorithm-based mutants. Such queries can determine whether or not the given combining algorithm is used correctly. Our empirical studies using various XACML policies have demonstrated that our approach is effective.

Role-based access control is an important access control method for securing computer systems. A role-based access control policy can be implemented incorrectly due to various reasons, such as programming errors. Defects in the implementation may lead to unauthorized access and security breaches. To reveal access control defects, this paper presents a model-based approach to automated generation of executable access control tests using predicate/transition nets. Role-permission test models are built by integrating declarative access control rules with functional test models or contracts (preconditions and postconditions) of the associated activities (the system functions). The access control tests are generated automatically from the test models to exercise the interactions of access control activities. They are transformed into executable code through a model-implementation mapping that maps the modeling elements to implementation constructs. The approach has been implemented in an industry-adopted test automation framework that supports the generation of test code in a variety of languages. The full model-based testing process has been applied to three systems implemented in Java. The effectiveness is evaluated through mutation analysis of role-based access control rules. The experiments show that the model-based approach is highly effective in detecting the seeded access control defects.

HPC typically employs parallelization in software and hardware in order to accelerate the computing processing. The underlying network itself is used collectively by all HPC experiments. In this paper, we propose a parallelization for the underlying network based on the different running HPC experiments or jobs. Each experiment/job will be logically sliced and isolated from other experiments. Additionally, each experiment/job includes different logical nodes across the HPC cluster. SDN controller is used to manage and control the slicing process. We evaluated this model using Opendaylight controller, FlowVisor and Mininet. We showed the impact that such network parallelization/slicing will bring to HPC clusters in terms of cluster efficiency and experiments' performance.

Data dependability is an important issue in data Grids. Replication schemes have been widely used in distributed systems to ensure availability and improve access performance. Alternatively, data partitioning schemes (secret sharing, erasure coding with encryption) can be used to provide availability and, in addition, to offer confidentiality protection. In peer-to-peer data Grids, such confidentiality protection is essential since the nodes hosting the data shares may not be trustworthy or may be compromised. However, difficulties in generating new shares and potential security concerns for share reallocation make a pure data partitioning scheme not easily adaptable to dynamic user access patterns. In this paper, we consider combining replication and data partitioning to assure data availability, confidentiality, load balance, and efficient access for data Grid applications. Data are partitioned and shares are dispersed. The shares may be replicated to achieve better performance, load balance, and availability. Models for assessing confidentiality, availability, load balance, and communication cost are developed and used as the metrics to guide placement decisions. Due to the nature of contradicting goals, we model the placement decision problem as a multi-objective problem and use a genetic algorithm to determine solutions that are approximate to the Pareto optimal placement solutions.

Software security issues have been a major concern in the cyberspace community, so a great deal of research on security testing has been performed, and various security testing techniques have been developed. Threat modeling provides a systematic way to identify threats that might compromise security, and it has been a well-accepted practice by the industry, but test case generation from threat models has not been addressed yet. Thus, in this paper, we propose a threat model-based security testing approach that automatically generates security test sequences from threat trees and transforms them into executable tests. The security testing approach we consider consists of three activities in large: building threat models with threat trees; generating security test sequences from threat trees; and creating executable test cases by considering valid and invalid inputs. To support our approach, we implemented security test generation techniques, and we also conducted an empirical study to assess the effectiveness of our approach. The results of our study show that our threat tree-based approach is effective in exposing vulnerabilities. Copyright © 2012 John Wiley & Sons, Ltd.

Functional modeling and safety analysis are two important aspects of safety-critical embedded systems. However, they are often conducted separately. In this paper, we present an approach for integrating fault-tree-based safety analysis into statechart-based functional modeling. The proposed approach uses systematic transformation steps that maintain the semantics of both the fault tree and the statechart. It also provides a set of conversion rules that transform the gates of fault trees into statechart notations. The resultant model shows how the system behaves when a failure condition occurs and acts as a basis model that ensures safety through requirement validation. Using the gas burner case study, we demonstrate the advantages of the integrated model over the use of separate models, such as the lack of ambiguities, separation of concerns, and taking the order of the occurrence of faults into consideration.

Aspect-oriented programming yields new types of programming faults due to the introduction of new constructs for dealing with crosscutting concerns. To reveal aspect faults, this paper presents a framework for testing whether or not aspect-oriented programs conform to their state models. It supports two families of strategies (i.e. structure-oriented and property-oriented) for automated generation of aspect tests from aspect-oriented state models. A structure-oriented testing strategy derives tests and test code from an aspect-oriented state model to meet a given structural coverage criterion, such as state coverage, transition coverage, or round trip. A property-oriented testing strategy generates test code from the counterexamples of model checking. Two such strategies are checking an aspect-oriented state model against trap properties and checking mutants of aspect models against system properties. Mutation analysis of aspect-oriented programs is used to evaluate the effectiveness of these testing strategies. The experiments demonstrate that testing aspect-oriented programs against their state models can detect many aspect faults. The comparative evaluations also reveal that the structure-oriented and property-oriented testing strategies complement each other—some aspect faults were detected by the structure-oriented strategies, but not by the property-oriented strategies and vice versa. Copyright © 2010 John Wiley & Sons, Ltd.

Poor design has been a major source of software security problems. Rigorous and designer-friendly methodologies for modeling and analyzing secure software are highly desirable. A formal method for software development, however, often suffers from a gap between the rigidity of the method and the informal nature of system requirements. To narrow this gap, this paper presents a UML-based framework for modeling and analyzing security threats (i.e. potential security attacks) rigorously and visually. We model the intended functions of a software application with UML statechart diagrams and the security threats with sequence diagrams, respectively. Statechart diagrams are automatically converted into a graph transformation system, which has a well-established theoretical foundation. Method invocations in a sequence diagram of a security threat are interpreted as a sequence of paired graph transformations. Therefore, the analysis of a security threat is conducted through simulating the state transitions from an initial state to a final state triggered by method invocations. In our approach, designers directly work with UML diagrams to visually model system behaviors and security threats while threats can still be rigorously analyzed based on graph transformation.

Aspect-oriented programming modularizes crosscutting concerns into aspects with the advice invoked at the specified points of program execution. Aspects can be used in a harmful way that invalidates desired properties and even destroys the conceptual integrity of programs. To assure the quality of an aspect-oriented system, rigorous analysis and design of aspects are highly desirable. In this paper, we present an approach to aspect-oriented modeling and verification with finite state machines. Our approach provides explicit notations (e.g., pointcut, advice and aspect) for capturing crosscutting concerns and incremental modification requirements with respect to class state models. For verification purposes, we compose the aspect models and class models in an aspect-oriented model through a weaving mechanism. Then we transform the woven models and the class models not affected by the aspects into FSP (Finite State Processes), which are to be checked by the LTSA (Labeled Transition System Analyzer) model checker against the desired system properties. We have applied our approach to the modeling and verification of three aspect-oriented systems. To further evaluate the effectiveness of verification, we created a large number of flawed aspect models and verified them against the system requirements. The results how that the verification has revealed all flawed models. This indicates that our approach is effective in quality assurance of aspect-oriented state models. As such, our approach can be used for model-checking state-based specification of aspect-oriented design and can uncover some system design problems before the system is implemented.

The Unified Modeling Language (UML) has been widely accepted as a standard for modeling software systems from various perspectives. The intuitive notations of UML diagrams greatly improve the communication among developers. However, the lack of a formal semantics makes it difficult to automate analysis and verification. This paper offers a graphical yet formal approach to specifying the behavioral semantics of statechart diagrams using graph transformation techniques. It supports many advanced features of statecharts, such as composite states, firing priority, history, junction, and choice. In our approach, a graph grammar is derived automatically from a state machine to summarize the hierarchy of states. Based on the graph grammar, the execution of a set of non-conflict state transitions is interpreted by a sequence of graph transformations. This facilitates verifying a design model against system requirements. To demonstrate our approach, we present a case study on a toll-gate system.

The new constructs in aspect-oriented programming bring new types of programming faults with respect to crosscutting concerns, such as incorrect pointcuts and advice. This paper presents a UML-based approach to testing whether or not an aspect-oriented program conforms to its expected crosscutting behavior. We explore aspect-oriented UML design models to derive tests for exercising interactions between aspects and classes. Each aspect-oriented model consists of class diagrams, aspect diagrams, and sequence diagrams. For a method under test, we weave the sequence diagrams of the advice on the method into the method's sequence diagram. Based on the woven sequence diagram and class/aspect diagrams, we then generate an AOF (Aspect-Object Flow) tree by applying coverage criteria such as condition coverage, polymorphic coverage, and loop coverage to woven sequence diagrams. In the AOF tree, each path from the root to a leaf is an abstract message sequence, indicating a template of test cases. A concrete test case is obtained by creating objects that satisfy the collective constraints in the template. Our empirical study shows that the model-based testing approach is capable of revealing several types of aspect-specific faults, including incorrect advice type, incorrect (weaker or stronger) pointcut strengths, and incorrect aspect precedence.

With the increasing complexity of software, new access control methods have emerged to deal with attribute- based authorization. As a standard language for attribute-based access control policies, XACML offers a number of rule and policy combining algorithms to meet different needs of policy composition. Due to their variety and complexity, however, it is not uncommon to apply combining algorithms incorrectly, which can lead to unauthorized access or denial of service. To solve this problem, this paper presents a fault-based testing approach for determining incorrect combining algorithms in XACML 3.0 policies. It exploits an efficient constraint solver to generate queries to which a given policy produces different responses than its combining algorithm-based mutants. Such queries can determine whether or not the given combining algorithm is used correctly. Our empirical studies using sizable XACML policies have demonstrated that our approach is effective.

Design-level vulnerabilities are a major source of security risks in software. To improve trustworthiness of software design, this paper presents a formal threat-driven approach, which explores explicit behaviors of security threats as the mediator between security goals and applications of security features. Security threats are potential attacks, i.e., misuses and anomalies that violate the security goals of systems' intended functions. Security threats suggest what, where, and how security features for threat mitigation should be applied. To specify the intended functions, security threats, and threat mitigations of a security design as a whole, we exploit aspect-oriented Petri nets as a unified formalism. Intended functions and security threats are modeled by Petri nets, whereas threat mitigations are modeled by Petri net-based aspects due to the incremental and crosscutting nature of security features. The unified formalism facilitates verifying correctness of security threats against intended functions and verifying absence of security threats from integrated functions and threat mitigations. As a result, our approach can make software design provably secured from anticipated security threats and, thus, reduce significant design-level vulnerabilities. We demonstrate our approach through a systematic case study on the threat-driven modeling and verification of a real-world shopping cart application.

How agents accomplish a goal task in a multi-agent system is usually specified by multi-agent plans built from basic actions (e.g. operators) of which the agents are capable. The plan specification provides the agents with a shared mental model for how they are supposed to collaborate with each other to achieve the common goal. Making sure that the plans are reliable and fit for the purpose for which they are designed is a critical problem with this approach. To address this problem, this paper presents a formal approach to modeling and analyzing multi-agent behaviors using Predicate/Transition (PrT) nets, a high- level formalism of Petri nets. We model a multi-agent problem by representing agent capabilities as transitions in PrT nets. To analyze a multi-agent PrT model, we adapt the planning graphs as a compact structure for reachability analysis, which is coherent to the concurrent semantics. We also demonstrate that one can analyze whether parallel actions specified in multi-agent plans can be executed in parallel and whether the plans can achieve the goal by analyzing the dependency relations among the transitions in the PrT model.

The process of agent migration is the major difference between logical code mobility of software agents and physical mobility of mobile nodes in ad hoc networks. Without considering agent transfer, it would make little sense to mention the modeling of strong code mobility, which aims to make a migrated agent restarted exactly from the state when it was stopped before migration. From the perspective of system's architecture, this paper proposes a two-layer approach for the formal modeling of logical agent mobility (LAM) using predicate/transition (PrT) nets. We view a mobile agent system as a set of agent spaces and agents could migrate from one space to another. Each agent space is explicitly abstracted to be a component, consisting of an environmental part and an internal connector dynamically binding agents with their environment. We use a system net, agent nets, and a connector net to model the environment, agents, and the connector, respectively. In particular, agent nets are packed up as parts of tokens in system nets, so that agent transfer and location change are naturally captured by transition firing (token game) in Petri nets. Agent nets themselves are active only at specific places and disabled at all the other places in a system net. The semantics of such a two-layer LAM model is defined by transforming it into a PrT net. This facilitates the analysis of several properties about location, state, and connection. In addition, this paper also presents a case study of modeling and analyzing an information retrieval system with mobile agents.

This paper presents an approach to the schedulability analysis of real-time systems modeled in time Petri nets by separating timing properties from other behavioral properties. The analysis of behavioral properties is conducted based on the reachability graph of the underlying Petri net, whereas timing constraints are checked in terms of absolute and relative firing domains. If a specific task execution is schedulable, we calculate the time span of the task execution, and pinpoint nonschedulable transitions to help adjust timing constraints. A technique for compositional timing analysis is also proposed to deal with complex task sequences, which not only improves efficiency but also facilitates the discussion of the reachability issue with regard to schedulability. We identified a class of well-structured time Petri nets such that their reachability can be easily analyzed.

Concurrence is an important research area in collaborative problem solving. This paper offers a formal definition for cooperative sequences in multi-agent systems, discusses the different categories of concurrent actions, and proposes some rules for situation revision and an algorithm used to generate resulting situations. An example is also given to show how to solve concurrent problems occurring in multi-agent systems.

This paper describes the declaration and inference based type system in an object-oriented logic framework, where logic objects are viewed as typed abstractions with state, constraints, behaviors and non-monotonic inheritance. Types are built by ordered constructors with subtyping relationships. As base types, the classes can be applied to complex type construction. Objects are classified according to their method signatures, and subtyping is independent of inheritance.

This paper presents a logic based language, SAFIN, for developing networked software agents. It integrates agent-oriented programming, KQML and basic mobile techniques to support intelligent behaviors, software interoperatablity and code transportability. As prototype based logic objects, agents are composed of network connections, knowledge bases (facts and beliefs), databases, behaviors, constraints, services, goals and KQML performatives. An approach to non-monotonic inheritance with both predicate level and clause level knowledge reuse is proposed and formally defined. Multi-level components and the interfaces to FTP services and relational database systems are also provided for developing specific distributed agents.

This article presents an object-oriented logic framework, LKO, for the dependable development of knowledge based systems. Based on logical objects which are viewed as abstractions with states, constraints, behaviors and nonmonotonic inheritance, a hybrid knowledge representation amalgamating rule, frame, semantics network and blackboard is available for both most structured and flat knowledge and requirements of knowledge based systems. After the iterations of specification modification and verification in terms of knowledge acquisition activities, prototypes are correctly formed. The LKO methodology, applying the concepts of rapid prototyping, top-down design and object-orientation, is designed to deal with changing and incomplete requirements and to provide multiple abstract models of the domain, where formal methods might be used at each abstract level.

In the process of software development, software testing is a huge project, and most of the software functionality testing is complex and repetitive, should to spend a lot of cost and manpower. Therefore, you can save a lot of manpower and costs, avoid human error and improve software quality if we can achieve automated testing. In the software development process, the application of model-driven developments has grown wider recently. The main concept is to fetch all of the significant properties referring to system design, and use formal or semi-formal model to describe system in different levels of abstraction. In this paper, we apply a tool based on high level Petri Net model of automated testing -- MISTA [1](Model based Integration and System Testing Automation) to automated generate test code for system. In this paper, through capture the information of the state machine diagram describes the behavior of the system in the Unified Modeling Language. Through the eXtensible Markup Language automation converted to High Level Petri Net test model, and then using automated test code generating software MISTA generation test cases and test code of system to achieve automated testing, and save the software required for testing a large number of human costs, and the software development process from design architecture to the software testing for a bridging.

This paper presents a declarative semantics of compositional inheritance in an object-oriented logic programming framework with explicit exceptions, based on the iterated least fixpoint semantics to normal logic programs. Taking logic objects with exceptions as a kind of non-monotonic theory, the non-monotonicity of inheritance is achieved, which is of importance for modeling incomplete knowledge and requirement specifications in both artificial intelligence and software engineering.

This paper presents an approach to non-monotonic inheritance in an object-oriented logic programming framework. Inheritance as sublation, achieved through predicate extension and exception, not only provides a very flexible mechanism for software reuse but also is very philosophical. Taking the (iterated least fixpoint) well-founded model semantics to traditional logic programs as a basis, the declarative semantics is also explored.

This paper presents a framework called logical knowledge object (LKO), which is taken as a basis of the dependable development of knowledge based systems(KBSs). LKO combines logic programming and object-oriented programming paradigms, where objects are viewed as abstractions with states, constraints, behaviors and inheritance. The operational semantics defined in the style of natural semantics is simple and clear. A hybrid knowledge representation amalgamating rule, frame, semantic network and blackboard is available for both most structured and flat knowledge. The management of knowledge bases has been formally specified. Accordingly, LKO is well suited for the formal representation of knowledge and requirements of KBSs. Based on the framework, verification techniques are also explored to enhance the analysis of requirement specifications and the validation of KBSs. In addition, LKO provides a methodology for the development of KBSs, applying the concepts of rapid prototyping and top-down design to deal with changing and incomplete requirements, and to provide multiple abstract models of the domain, where formal methods might be used at each abstract level.

This paper presents a novel programming language called LOC (Logical Objects with Constraints), which combines logic programming and object-oriented programming paradigms. In LOC, logical objects are viewed as abstractions with state, constraints, behaviors and inheritance. It therefore supports such notions as inheritance, modularity and reusability, which have turned out to be extremely useful for large scale software systems. The operational interpretation defined in the style of natural semantics is simple and clear. The transformation of LOC into Prolog is also explored to indirectly illustrate the descriptive semantics.

Security has become a priority for software development and many security testing techniques have been developed over the years. Benchmarks based on real-world systems, however, are in great demand for evaluating the vulnerability detection capability of these techniques. To develop such a benchmark, this paper presents an approach to security mutation analysis of FileZilla Server, a popular FTP server implementation as a case study. In the existing mutation testing research, mutants are created through syntactic changes. Such syntactic changes may not result in meaningful security vulnerabilities in security-intensive software. Our approach creates security mutants by considering the causes and consequences of vulnerabilities. The causes of vulnerabilities include design-level (e.g., incorrect policy enforcement) and implementation-level defects (such programming errors as buffer overflow and unsafe function calls). The consequences of vulnerabilities refer to various potential attacks, such as spoofing, tampering, repudiation, information disclosure, denial of service, and elevation of privilege (STRIDE). Using this approach, we have created 30 distinct mutants for FileZilla Server. They have been applied to the evaluation of two security testing methods that use attack trees and attack nets as threat models for test generation. The results show that, while these testing methods can kill most of the mutants, they have an important limitation -- they cannot detect the vulnerabilities that are not captured by the threat models.

Since the launch of the first IEEE/ACM International Workshop on Automation of Software Test eight years ago, the research in the area has developed rapidly as test automation has become a mature practice widely adopted by the IT and software industry. One of the goals that has been continuously pursued is to bridge the gap between research and practice. Many of the recent papers are closely related to the current practice in the industry reflecting the trend toward a mature community unifying both researchers and practitioners. This is also reflected in the diversity of the topics related to the practical industrial problems covered in this special section. Authorization systems are at the heart of computer security. Antonia Bertolino et al.’s paper entitled Testing of PolPA-based Usage Control Systems is devoted to the testing of the Policy Decision Point (PDP) within the authorization system called PolPA, which enables both history-based and usage-based control of accesses. They propose two testing strategies for validating the history-based access control and the usage control functionalities, respectively. The former is based on a fault model being able to highlight the problems and vulnerabilities that could occur during the PDP implementation. The latter combines the standard technique for condition coverage with a methodology for simulating the continuous control of the PDP

A formal method for software development often introduces a gap between rigidity of the method and informal nature of system requirements. This paper presents a UML-based framework for design and analysis of dependable software while narrowing such a gap. We model the intended functions of a software application with UML statecharts and security threats, i.e., potential attacks, with sequence diagrams. The statechart diagrams are converted into a graph transformation system, which is a well-studied formal method. This allows security threats to be verified against intended functions.

As software systems are encompassing a wide range of fields and applications, software reliability becomes a crucial step. The need for safety analysis and test cases that have high probability to uncover plausible faults are necessities in proving software quality. System models that represent only the operational behavioral of a system are incomplete sources for deriving test cases and performing safety analysis before the implementation process. Therefore, a system model that encompasses faults is required. This paper presents a technique that formalizes a safety model through the incorporation of faults with system specifications. The technique focuses on introducing semantic faults through the integration of fault trees with system specifications or statechart. The method uses a set of systematic transformation rules that tries to maintain the semantics of both fault trees and statechart representations during the transformation of fault trees into statechart notations.

This paper presents a formal approach to threat-driven modeling and verification of secure software using aspect-oriented Petri nets. Based on the behavior model of intended functions, we identify and build formal models of security threats, which are potential misuses and anomalies of the intended functions that violate security goals. Threat mitigations are further modeled in an aspect-oriented paradigm. Taking Petri nets as a formal basis for modeling behaviors, threats, and mitigations as a whole, we verify properties of and consistency between behaviors and threats, and absence of identified threats from the integrated model of functions and threat mitigations. This makes it possible to achieve a design that is provably resistant to the anticipated threats and thus reduce significant design-level vulnerabilities.

This paper presents an aspect-oriented approach to integrated specification of functional and security requirements based on use-case-driven software development. It relies on explicit identification of security threats and threat mitigations. We first identify security threats with respect to use-case based functional requirements in terms of security goals and the STRIDE category. Then, we suggest threat mitigations for preventing or reducing security threats. To capture the crosscutting nature of threats and mitigations, we specify them as aspects that encapsulate pointcuts and advice. This provides a structured way for separating functional and security concerns and for analysing the interaction between them.

Sense and Respond Logistics (SARL) is a highly flexible, agile, and adaptive methodology for managing logistics resources in a network-centric and information rich environment. Designing and developing the software for simulating a system with such complexity presents challenges that stem from the role of heterogeneous communication channels and decision choices that produce non-deterministic outcomes. We describe the use of multi-agent approaches for simulating SARL applications. We also argue for the use of formal methods and aspect-oriented techniques in the design of these simulations, to assist in supporting model validation and verification. Features of an aspect-oriented, multi-agent, architectural description languages are also presented as a mechanism for reasoning about cross-cutting concerns.