Major Advisor: John Hatcliff
Committee members: Matt Dwyer, Bill Hankley
10/22/2003
Phase1: Overview and requirement
Phase3: Implementation, testing, and documentation
Appendix A: CAD grammar
Appendix B: an example of assembly code
Appendix C: Alloy model
I could not finish this project without the help from many people.
First, I thank our team members, Qiang Zeng, Prashant Shanti Kumar, Adam Childs, Jesse Greenwald, and Venkatesh Prasad Ranganath. They all provided precious comments and help on my project. Qiang Zeng and Prashant Shanti Kumar explained the requirement patiently. Jesse Greenwald carefully reviewed my source code.
Second, I thank Dr.Dwyer and Dr.Hankley for their helpful comments and suggestions, and for being my committee.
Third, I thank my major advisor, Dr.Hatcliff. He not only gave me the right direction on my whole project, but also helped me on how to build presentation slides. Whithout those help, I could not give my presentations smoothly.
Finally, and most importantly, I thank my husband, William Deng. He has provided help, encouragement, support, patience, and, above all, Love.
Shufeng Li
10/22/2003
The use of component models such as SUN Microsystems’s Enterprise Java Beans, Microsoft’s Component Object Model, Microsoft’s .NET Framework, and CORBA Component Model (CCM) in large scaled distributed software is expanding rapidly. For embedded safety-critical and mission-critical applications, the high-assurance of productivity and reliability is required. However, there is little support for helping programmers write high reliability distributed applications.
At Kansas State University, Cadena is being developed to form an effective basis for development of such systems. It is an integrated environment for real-world experimentation with technologies for high-assurance distributed systems built using CORBA Component Model [5]. It employs light-weighted specification, analysis, and verification techniques.
The following are the features that Cadena provides:
· Allows user to design CORBA Component Model (CCM) by using CCM Interface Definition Language (IDL).
· Allows user to create system configurations.
· Allows user to reason about component dependency and synthesize dependency-based real-time and distribution aspect information.
· Allows user to specify component behavioral descriptions.
· Allows user to model check behavioral descriptions.
CORBA Component Model (CCM) is a distributed component-oriented model. CCM IDL is a very high-level specification language which specifies the component interfaces, such as, what a component offers to other components, what a component requires from other components, what the business life cycle operations are (i.e. home).
A running example from Boeing Boldstrok will be used to illustrate these features. Figure 1 presents the CCM architecture for the example system. The system is realized as a collection of components coupled together via interfaces and event connections. Figure 2 gives the CCM IDL that defines the component type BMLazyActive.
Figure 1: Simple avionics system
#pragma prefix "cadena"
module common {
interface ReadData {
readonly attribute any data;
};
eventtype DataAvailable {};
enum LazyActiveMode {fresh, stale};
component BMLazyActive {
provides ReadData dataOut;
uses ReadData dataIn;
publishes DataAvailable outDataAvailable;
consumes DataAvailable inDataAvailable;
attribute LazyActiveMode dataStatus;
};
home BMLazyActiveHome manages BMLazyActive { };
Figure 2: BMLazyActive, a CCM/Cadena artifact, for ModalSP (excerpts)
A component is a meta-type which groups attributes and port interfaces together. Attributes are named variables to express component configurable properties and exposed though accessors and mutators. Ports define interfaces that are provided or used by components or other elements. Facets, receptacles, event sources, and event sinks are the four kinds of ports defined in component types by CCM. Component home is another meta-type defined in CCM. A component home is the component factory of a given component type instances.
Facets are distinct interfaces provided by a component for client interaction. They present the functional behaviors of components during normal execution. Keyword “provides” is used to define a facet.
Receptacles provide a way for components to accept object references (i.e. facet references) in order to use its operations. Keyword “uses” is used to define a receptacle.
Event source is used when components can provide a kind of event. Event sink is used when component can accept some kind of events. There are two kinds of event source: emits and publishes. An emits event source works on a one-to-one relationship. Only one consumer can connect to it at a time. A publishes event source works on a one-to-many relationship. A limited number of consumers can connect to it at a time. Keyword “emits” is used to define an emits event source, “publishes” is used to define a publishes event source.
An event sink allows a component receives events of a certain type. Keyword “consumes” is used to define an event sink.
For facets and receptacles, all the interface types should be valid. For example, the ReadData is an interface type defined previously. For event source and event sink, all the event type should be valid. For example, DataAvailable is an event type defined previously.
A home definition describes an interface which is a given component type factory, which controls component instances’ creation, destruction, or finding. Keyword “home” is used to define a home, and keyword “manages” describes what kind of component this home manages.
As depicted in figure 2, dataOut, dataIn, outDataAvailable, and inDataAvailable are a facet, a receptacle, an event source, and an event sink, respectively. BMLazyActiveHome is the home for BMLazyActive component.
Figure 3 [5] displays the internal structure of Cadena toolset. The Cadena project contains four high-level specification forms: a CORBA IDL file that defines the structure of the component types (like those in figure 2), a Cadena Property Specification (CPS) file that specifies various aspects of component behavior, a Cadena Assembly Description (CAD) that specifies the component instances that form the system and the connections among them, and a specification file that stores the information about the desired the correctness properties of the system [5]. The boxes of IR3, IDL2Java, stubs, skeletons, and Implementation are all related to OpenCCM, the first public available Java implementation of CCM. The input files are created by the Editor that is built by the IBM Eclipse plug-in facilities. In particular, the CAD format has textual editor, and form based graphical editor. The Dependency analyzer analyzes the component dependency based on the CAD specification file and CPS. The deployment Java code generator generates the system assembly code for component allocation and connections.
Figure 3: Cadena Architecture
In figure 3, the CAD compiler is responsible for compiling the CAD/scenario file and creating an Abstract Syntax Tree (AST) that contains the component deployment and assembly information. My project, the deployment generator of Cadena, shall take the AST, and generate JAVA component assembly code that will assign homes, create component instances, and connect these instances for the user.
For large scaled systems, the component deployment and assembly processes are complex even if the user is familiar with all the implementation detail. They include how and where these facilities, which holds components and homes, installed, how the component homes are created and installed, how the component instances are created and installed and how they connect with each other, and when the configuration is completed. My project will carry out all these processes based on a simply property file created by the user. The main benefit of this project is to increase the productivity of programmer, reduce the complexity to implement large distributed systems, reduce the skills requirement, and improve software quality.
This project follows the deployment process defined by CCM. It uses the ComponentInstallation object and interacts with the user to acquire information of the target hosts of the deployment. The AssemblyFactory is used to create Assembly object that will be used later. To create a component instance, the Assembly object creates a container server called the ComponentServer, then a Container is instantiated on the container server, the container provides an operation to install a component home, and finally the component instance is created by its component home. So the generated deployment code structure is like this process. The target host information is obtained from a property created by user [10].
The JAVA Implementation of IDL Configuration (JIIC) project consists of three components. One component is responsible for automatically generating Java assembly code, OEP XML configuration file, and KSU Event Service configurationXML file, respectively. All these components shall get the information from the Cadena configuration scenario files and some property files.
This document is used during the specification process. It is the baseline for developing the software. It will also be used in validating and testing the project. The project shall meet all the requirements in this document.
The JIIC Software Requirements Specification defines and describes the functions, interfaces, and performance of JIIC project.
The benefit of the project will be reducing the implementation time of generating assembly code. So user could just focus on domain or business functional development.
JIIC: JAVA Implementation of IDL Configuration
CCM: CORBA Component Model
IDL: Interface Definition Language
OpenCCM: Open CORBA Component Model
ORB: Object Request Broker
IR: Interface Repository
AST: Abstract Syntax Tree
CORBA Component Model: Discussion and Use with OpenCCM, Raphaël Marvie, Philippe Merle
The rest of this document describes the project and its requirements. Section 2 is the overall descriptions of the project. Specific requirements are defined in Section 3.
This section provides an overview of the key JIIC project requirements. It is intended for general information only, and does not describe all of the details of the various issues, which will be provided in Section 3.
The JIIC project will work together with OpenCCM-0.5 and OpenORB-1.3.1. It is not part of them, but its functionality, performance, and behavior will depend on them. It shall also be integrated by IBM Eclipse, which the user interface will depend on.
In this project, there are several components working together. Operating system controls all the software products and logic files. OpenCCM compiler compiles the input IDL files. Its generators generate java skeletons, stubs, and implementation files associated with objects in the IDL files. JIIC gets and analyzes scenario files, which are provided by user and expressed in AST, or configuration files in XML format, extracts configuration information, and generates Java assembly file and/or executable scripts based on those files generated by OpenCCM generator.
a) Operating system:
1) Read file
2) Write file
b) OpenCCM-0.5:
1) Compile IDL file
2) Generate Java stubs and skeletons interfaces
3) Generate Java implementation files
c) Bold stroke:
1) Generate scenario AST for this product to use
d) JIIC product:
1) Generate Java assembly code based on those files generated by OpenCCM and scenario files. It shall follow OpenCCM naming rules.
2) Generate OEP XML configuration file based on scenario files.
3) Generate KSU Event Service configuration XML file based on scenario file.
2.2.2.2 User interfaces:
This product shall be integrated with Eclipse environment. The user interface shall follow the Cadena system user interface requirement. All the three generation operations shall be done by clicking buttons. Then the user will follow the prompt to input the output file names, the input scenario files, input cps files, and other information if needed.
2.2.2.3 Hardware Interfaces N/A
2.2.2.4 Software interfaces:
a) Operation system: Microsoft Windows 98 or above, Linux, or UNIX.
b)
OpenCCM-0.5:
/ccm/OpenCCM-0.5
c)
OpenORB-1.3.0 or later:
/ccm/OpenCCM-0.5/OpenORB-1.3.0
d) Ant-1.4 or later http://jakarta.apache.org/ant/
2.2.2.5 Memory constraints: 64M
2.2.2.6 Operations:
a) The generated assembly code shall be written into the current directory or into the directory as the user required.
b) XML configuration files shall be written into the directory with the name as user required.
c) Backup and recovery: if bad things happen, all files provided by user shall not be damaged.
This product has three main functions. Each function is represented by an output file. Figure 4 is the use case.
1) xecutable java assembly file
2) adena configuration file
3) Facet integration configuration file
Figure 4 Component Assembly Description Compiler
User should be familiar with CORBA and CCM, know how to install OpenCCM on Windows or UNIX platform, know how to use ant and write build.xml file.
a) This product needs to work with OpenCCM and ORB. It must follow their rules.
b) Many configuration and deployment information are flexible.
c) The assembly code will work on distributed operating system, reliability and security is required.
a) We assume that the OpenCCM compiler and generators work correctly.
b) We assume that the JIIC tool will work with OpenCCM.
c) The output assembly file depends on user’s configuration file.
This section describes the details of the requirements specifications for developer and user to understand the product and communicate with each other. Testers should also test this product against this section mainly.
1) XML configuration file
a) description of purpose: contains all components and deployment information
b) source of input: from the command line as a parameter
c) relationships to other outputs: the base of assembly code
2) Scenario file
a) description of purpose: contains component instance and connection information
b) source of input: from the command line as a parameter
c) relationships to other outputs: the instance creation and connection information of assembly code comes from this file
3) package name of generated assembly code
a) description of purpose: the package name of assembly code
b) source of input: input by user from keyboard
c) valid range: a valid or empty string, each word is separated by a dot
d) relationships to other outputs: package name of assembly code
4) location of assembly code
a) description of purpose: the folder where the assembly code is located
b) source of input: input by user from keyboard
c) valid range: a single valid word, not empty
d) relationships to other outputs: folder name of assembly code
5) deployment file
a) description of purpose: the deployment information of component instances and homes
b) source of input: from the command line as a parameter
c) relationships to other outputs: the home assignment information of assembly code comes from this file
A. Stimulus 1: generate code by visiting AST
1) Function 1: get AST from a scenario file
a) Validity checks on the inputs
· The file exists
b) Exact sequence of operations
· Get AST
· Close scenario file
· Return AST
c) Responses to abnormal situations
· Throw exceptions
· Return null
· Terminate program
2) Function 2: take deployment file
a) Validity checks on the inputs
· The file exists
b) Exact sequence of operations
· Get deployment information map
· Close deployment file
c) Responses to abnormal situations
· Throw exceptions
· Terminate program
3) Function 3: Take user inputs
a) Validity checks on the inputs
· Location folder is a valid string
· Location folder is not empty
· Package name is a valid string, each word is separated by a dot
b) Exact sequence of operations
· Assign location folder name and package name to variables.
· Begin to generate assembly code
c) Responses to abnormal situations
· Ask user again
· Accept the inputs
4) Function 4: generate assembly code
a) Exact sequence of operations
· Open output file
· Initialize file header
· Create homes and components
· Connect clients and server
· Configuration completion
· Close output file
b) Responses to abnormal situations
· Throw exceptions
· Terminate program
B. Stimulus 2: generate code by visiting XML configuration code
1) Function 1: get AST from a XML configuration file
a) Validity checks on the inputs
· The file exists
b) Exact sequence of operations
· Open file
· Get AST
· Close file
· Return AST
c) Responses to abnormal situations
· Throw exceptions
· Return null
· Terminate program
Note: other functions are the same as function2, function3, and function4 in stimulus 1.
a) number of simultaneous users to be supported: 1
b) amount and type of information to be handled:
Static information:
1) XML configuration file: logic file
2) scenario file: logic file
3) deployment file: logic file
Dynamic information:
1) package name of assembly code
2) folder name of assembly code
3) Output file name
a) Types of information used by various functions:
XML configuration file, scenario file, deployment file, assembly code, and CPS file.
b) Frequency of use:
All information will be in use for every execution.
c) Accessing capabilities:
Users can read or modify XML configuration file, scenario file, and deployment. Assembly code is generated under user’s control. And user can read or modify the assembly code.
a) Report format: assembly code shall be in the format of Java file
b) Data naming: data naming rules shall follow the rules of OpenCCM
a) Reliability: this product shall always be reliable if no other bad things happen
b) Security: if user input something wrong, all existing files shall not be lost
c) Portability: percentage of code that is host dependent: 0%
Use of a proven portable language: Java
Use of particular language: IDL
This specific requirement is organized in stimulus mode.
2.4.1.1 Interface Definition Language (IDL3) input file
#pragma prefix "cis.ksu.edu"
module exmpl {
//interface definition
//used for facets and receptacles
interface ReadData {
readonly attribute any data;
};
//event type definition
//used for event source and event sink
eventtype DataAvailable {};
//component BMLazyActive definition
component BMLazyActive {
provides ReadData dataOut;
uses ReadData dataIn;
publishes DataAvailable outDataAvailable;
consumes DataAvailable inDataAvailable;
};
//component home definition
home BMLazyActiveHome manages BMLazyActive
{ };
//component BMDevice definition
component BMDevice : NamedComponent {
provides ReadData dataOut;
publishes DataAvailable outDataAvailable;
consumes TimeOut timeOut;
};
//component home definition
home BMDeviceHome manages BMDevice
{ };
};
2.4.2.2 Component Assembly Description (CAD) input file
a) Assumption about the CAD file
· The system name is defined. It is can not be empty.
· The importLibs are well defined and completed.
· The locations are well defined and completed. The location list can not be empty.
· Component interfaces are well defined. The instance declaration list can not be empty. An interface is allowed to have no connection declarations.
· The connections are well defined in each component interface. Facets and receptacles, event suppliers and event consumers are well defined.
b) An simple example
system ModalSPScenario {
…
//Run rate declarations
Rates 20, 5, 1;
//location declarations
Locations Board1, Board2;
//component instance declaration
//in which the connections with other component instances shall be declared
Instance GPS implements BMDevice on Board1 {
}
Instance AirFrame implements BMLazyActive on Board2 {
//event source-sink definition, related to 4.2.9
connect this.inDataAvailable to GPS.outDataAvailable;
//receptacle-facet definition, related to 4.2.9
connect this.dataIn to GPS.dataOut;
}
…
}
There are several steps to be done in the assembly code. These steps should be followed one by one.
ORB is an essential part for CORBA. It has to be initialized. The statement to initialize ORB is as the following:
org.omg.CORBA.ORB orb = org.objectweb.ccm.Components.Runtime.init(args);
2.4.2.2 Obtain the Name Service
The command for obtaining the name server is the following:
org.omg.CORBA.Object obj = orb.resolve_initial_references("NameService");
org.omg.CosNaming.NamingContext nc =
org.omg.CosNaming.NamingContextHelper.narrow(obj);
Figure 5 Component Deployment Process
Figure 5 [5] is the component deployment process.
· ComponentInstallation, singleton, purpose is to install component implementations.
· AssemblyFactory, singleton, purpose is to create Assembly objects
· Assembly, represents an assembly instantiation, purpose is to coordinates the creation and destruction of component assemblies and components
· ServerActivator, singleton by host, purpose is to create ComponentServer objects
· ComponentServer, purpose is to create Container objects
· Container, purpose is to install CCMHome objects
The following steps, 4.1.3 to 4.1.7, follow the process.
2.4.2.3 Obtain Component Servers
The component server acts as a singleton factory for the creation of Container objects and is used by an Assembly object during the deployment process. [2] The component servers need to be configured according to the program requirements. For example, if you need two component servers, you have to obtain two. The component servers have to be started before component assembly code runs. We will introduce how and where to start the component servers later. In our example, we have two Component servers: ComponentServer1 and ComponentServer2. The statements to obtain component server1 and component server2 are listed as followings:
org.omg.CosNaming.NameComponent[] ncomp = new org.omg.CosNaming.NameComponent[1];
ncomp[0] = new
org.omg.CosNaming.NameComponent("ComponentServer1", "");
obj = nc.resolve(ncomp);
org.objectweb.ccm.Deployment.Server server1 =
org.objectweb.ccm.Deployment.ServerHelper.narrow(obj);
ncomp[0].id = "ComponentServer2";
obj = nc.resolve(ncomp);
org.objectweb.ccm.Deployment.Server server2 =
org.objectweb.ccm.Deployment.ServerHelper.narrow(obj);
2.4.2.4 Obtain the container homes and archive installators.
The container homes and archive installators need to be get from component servers above. The followings are the commands in our example:
org.omg.Components.Deployment.ComponentServer server1_cs = server1.provide_component_server();
org.omg.Components.Deployment.ComponentServer server2_cs = server2.provide_component_server();
org.omg.Components.Deployment.ComponentInstallation server1_inst = server1.provide_install();
org.omg.Components.Deployment.ComponentInstallation server2_inst = server2.provide_install();
To make program running, two archives are needed. One is called “OpenCCM_Plugins.jar” that is available at the demo/demo1 directory and should be copied into the current directory. The other one is created when you use ant to build the project. You have to install these two archives on each container home that just obtained at the previous step.
server1_inst.install("exmpl", "./archives/exmpl.jar");
server2_inst.install("exmpl", "./archives/exmpl.jar");
// install some plugins already provided by OpenCCM.
server1_inst.install("openccm_plugins", "./OpenCCM_Plugins.jar");
server2_inst.install("openccm_plugins", "./OpenCCM_Plugins.jar");
2.4.2.6 Declare deployment container
Deployment containers can be got from the container homes above. In our example, we have two containers:
org.omg.Components.Deployment.Container server1_cont =
server1_cs.create_container(new org.omg.Components.ConfigValue[0]);
org.omg.Components.Deployment.Container server2_cont =
server2_cs.create_container(new org.omg.Components.ConfigValue[0]);
After containers are created, component homes can be installed on them. For a home, which container it should be installed on depends on the user deployment information. There is only one component home in our example, we can install it on either of the two servers. The following code shows that it is installed on server2.
org.omg.Components.CCMHome h = server2_cont.install_home("exmpl",
"edu.ksu.cis.BMLazyActiveHomeImpl.create_home", new org.omg.Components.ConfigValue[0]);
BMLazyActiveHome lazyactivehome = BMLazyActiveHomeHelper.narrow(h);
BMDeviceHome bmdevicehome = BMDeviceHomeHelper.narrow(h);
After a component home is created, the corresponding component can be created. The following is the BMLazyActive component creation:
BMLazyActive lazyactive = lazyactivehome.create();
BMDevice bmdevice = bmdevicehome.create();
2.4.2.9 Connect ports
Once all components are installed, the components can be connected together according to the scenario information. This is done by connecting receptacles with facets, and event sinks with event source.
Receptacle-Facet connection:
airframe.connect_dataIn(gps.provide_dataOut());
Event source-sink connection:
gps.subscribe_outDataAvailable(airframe.get_consumer_inDataAvailable());
2.4.2.10 Configuration complete
After the connection operations, the configuration_complete() of each component can be called to notify that all configuration and initialization are done. This is the command in our example:
lazyactive.configuration_complete();
This project is divided into three
phases:
Phase I: Specification: Expected to be finished by 10/15/2002
1. Overview of
project: 6/24/2002 to 7/26/2002
Study CCM concepts, write project overview, including project statement, purpose
and goals.
2. Project
plan: 7/17/2002 to 7/22/2002
Break this project into more details, and set up milestones.
3. Requirement:
7/22/2002 to 8/12/2002
Specify requirements.
4. Cost
estimation: 8/12/2002 to 8/20/2002
Estimate the size and effort needed for the project.
5. Presentation I: expected by 10/15/2002
Phase II: Design: Expected to finish by 11/22/2002
Phase III: Implementation, Testing and Documentation: Expected to finish by 4/10/2003
The total line of code (LOC) is expected around 4500. Based on requirement, the program is broken into to parts:
Based on AST: 500 lines – does not support event correlation yet, estimation for correlation is about 100 lines.
Based on the XML configuration file: 4000 lines (estimation is based on other people’s experience in our group)
Effort = 2.4 * (4.5)1.05 = 11.6
Development time = 2.5 * (11.6)0.38 = 6.35 (months)
|
|
Simple |
Average |
Complex |
Subtotal |
|||
|
Count |
Weights |
Count |
Weights |
Count |
Weights |
||
|
Inputs |
2 |
3 |
0 |
4 |
0 |
6 |
3 |
|
Outputs |
3 |
4 |
0 |
5 |
0 |
7 |
12 |
|
Inquiries |
0 |
4 |
0 |
5 |
0 |
7 |
0 |
|
Files |
1 |
7 |
0 |
10 |
3 |
15 |
52 |
|
Interfaces |
0 |
5 |
1 |
7 |
1 |
10 |
17 |
|
Total |
|
|
|
|
|
|
84 |
|
Complexity Weighting Factors |
Rate (1-5) |
|
Does the system require reliable backup and recovery |
1 |
|
Are data communications required? |
2 |
|
Are there distributed processing functions |
3 |
|
Is performance critical |
1 |
|
Will the system run in an existing, heavily utilized operational environment |
3 |
|
Does the system require on-line data entry? |
1 |
|
Does the on-line data entry require the input transaction to be built over multiple screens or operations |
0 |
|
Are the master files updated on-line |
0 |
|
Are the inputs, outputs, files, or inquiries complex |
5 |
|
Is the internal processing complex |
5 |
|
Is the code designed to be reusable |
3 |
|
Are conversion and installation included in the design |
3 |
|
Is the system designed for multiple installations in different organizations |
5 |
|
Is the application designed to facilitate change and ease of use by the user |
5 |
|
Sum |
37 |
Adjusted FP
= FPunadjusted*(.65+.01*sum of ratings)
= 84 * (.65+.01*37)
= 85.68
This document is mainly based on the Assignment 1 and Assignment 2 of CIS771, Software Specification, which was taught by Dr.Hatcliff. Most of the structures and constraints are followed the homework requirements.
The structure of CCM components is specified using the CCM Interface Definition Language (IDL). The listing below shows the CCM IDL for two of the component schemas (BMLazyActive and BMModal1) used in the example system.
module modalsp {
interface ReadData {
readonly attribute any data;
};
eventtype TimeOut {};
eventtype DataAvailable {};
enum LazyActiveMode {stale, fresh};
component BMLazyActive {
provides ReadData dataOut;
uses ReadData dataIn;
publishes DataAvailable outDataAvailable;
consumes DataAvailable inDataAvailable;
};
enum OnOffMode {enabled, disabled};
interface ChangeMode {
attribute OnOffMode modeVar;
};
component BMModal1 {
provides ChangeMode modeChange;
provides ReadData dataOut;
uses ReadData dataIn;
publishes DataAvailable outDataAvailable;
consumes DataAvailable inDataAvailable;
};
};
CCM components “provides” interfaces to clients on ports referred to as “facets”, and “uses” interfaces provided by other clients on ports referred to as “receptacles”. Components “publishes” events on ports referred to as “event sources”, and “consumes” events on ports referred to as “event sinks”.
A CCM system is built by creating “instances” of the component schemas above and by connecting the ports of these instances together. For example, below is a fragment of the system construction script that our tools use for building the example system.
system ModalSPScenario {
...
Instance AirFrame implements BMLazyActive {
connect this.inDataAvailable
to GPS.outDataAvailable
connect this.dataIn to GPS.dataOut;
}
Instance TacticalSteering implements BMModal1 {
connect this.inDataAvailable
to AirFrame.outDataAvailable;
connect this.dataIn to AirFrame.dataOut;
}
...
The relationship between component schemas and component instances is analogous to the relationship between classes and objects in conventional OO languages. In OO languages, one creates an object as an instance of a particular class; in component models like CCM, one creates a component instance that is an instance of a particular component schema. In CCM, one then connects, e.g., a port p1 of one instance to a port p2 of another instances if p1 and p2 are type and kind compatible. Kind compatible means the following: a facet port can only connect to a receptacle port, and an event source port can only connect to an event sink port. Type compatible means that on an interface (i.e., facet/receptacle) connection, the interface type of the connecting ports must match, and on an event source/sink connection, the event type of the connecting ports must match.
Structure1: Five basic signatures are defined to represent the following entities: component schemas, port schemas, component instances, port instances, and port types.
--signature of ComponentSchema
sig ComponentSchema {schemaPorts: set PortSchema}
--signature of PortSchema
sig PortSchema {ptype: PortType, schemaPortOf: ComponentSchema}
--signature of ComponentInstance
sig ComponentInstance {}
--signature of PortInstance
sig PortInstance {}
--signature of PortType
sig PortType {}
Note: we are abstracting away multiple details when modeling in Alloy. First, we do not need to consider actual component schema names (e.g., BMLazyActive) -- we can't do this any way in Alloy since it doesn't have strings. We will only rely on the fact that there are distinct component schemas that we can compare for equality.
Structure2: There are four kinds of ports: facet, receptacle, source, and sink.
part sig Facet, Receptacle, Source, Sink extends PortSchema {}
Structure3: There are two kinds of port types: event, interface.
part sig EventType, InterfaceType extends PortType {}
According to the implicit facts of signature declaration in Alloy, the following constraints defined automatically
Structure4: Each component schema has zero or more port schemas.
Structure5: Each port schema belongs to one component schema.
Structure6: Each port schema has one type.
In addition to these basic signatures, another signature, “state”, is defined to help modeling the dynamic specifications later. Part of the declaration of “state” signature is listed following:
sig State {
setComponentInstances : set ComponentInstance,
setPortInstances : set PortInstance,
componentInstanceOf : ComponentInstance -> ?ComponentSchema,
componentInstances : ComponentSchema? -> ComponentInstance,
portInstanceOf : PortInstance -> ?PortSchema,
portInstances : PortSchema? -> PortInstance,
instancePorts : ComponentInstance? -> PortInstance,
instancePartOf: PortInstance -> ?ComponentInstance,
connection : PortInstance -> PortInstance
}{…}
In this signature, some basic constraints are defined though the implicit facts.
Structure7: Port instances can connect to other port instances.
connection : PortInstance -> PortInstance
The “state” signature represents the current of this model. If anything is changed, the “state” should be changed according. Since ComponentInstance and PortInstance could be created, destroyed, or connected to other Instances, the dynamic relationship between instances and schemas is captured in this signature.
Structure8: Each component instance in this state has exactly one Component schema, others don't have Component schema.
all ci: setComponentInstances |
one componentInstanceOf[ci]
all ci: ComponentInstance - setComponentInstances |
no componentInstanceOf[ci]
Structure9: Each port instance in this state has exactly one Port Schema,
others don't have Port Schema.
all pi: setPortInstances |
one portInstanceOf[pi]
all pi: PortInstance - setPortInstances |
no portInstanceOf[pi]
Structure10: Each component instance has zero or more port instances.
instancePorts : ComponentInstance? -> PortInstance,
Structure11: Each port instance in this state has exactly one Component instance which also belongs to this state, others don't have Component instance.
all pi: setPortInstances |
(one instancePartOf[pi]) && (instancePartOf[pi] in setComponentInstances)
all pi: PortInstance - setPortInstances | no instancePartOf[pi]
Constraint1: Facet and receptacles must have “interface” port types
Constraint2: Event source and sink ports must have “event” port types
fact typechecking {
// Constraint.1
// facets/receptacles have interface types
all p : Facet + Receptacle | p.ptype in InterfaceType
// Constraint.2
// source/sinks have event types
all p : Source + Sink | p.ptype in EventType
}
Constraint3: Each port instance pi of a component instance ci have a corresponding port schema ps in the component schema cs associated with ci.
all ci : setComponentInstances |
all pi : instancePorts[ci] |
portInstanceOf[pi] in (componentInstanceOf[ci]).schemaPorts
Constraint4: Conversely, each port schema ps declared in a component schema cs must have a corresponding port instance pi in every component instance ci of cs.
all ci : setComponentInstances |
all ps : (componentInstanceOf[ci]).schemaPorts |
one pi : portInstances[ps] | instancePartOf[pi] = ci
Constraint5: The port instance 'connection' relation should be symmetric.
all pi1 : setPortInstances |
all pi2 : connection[pi1] | (pi1 in connection[pi2])
AConstraint1: If two port instances belong to the same component instance, they cannot be connected.
all pi : setPortInstances |
all p: connection[pi] |
not instancePartOf[pi] = instancePartOf[p]
AConstraint2: Facet port instances should only connect to receptacle port instances (and vice versa).
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Facet => all pi : portInstances[ps] |
all pc: connection[pi] |
portInstanceOf[pc] in Receptacle)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Receptacle => all pi : portInstances[ps] |
all pc: connection[pi] | portInstanceOf[pc] in Facet)
AConstraint3: Event source port instances should only connect to event sink port instances (and vice versa).
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Source => all pi : portInstances[ps] |
all pc: connection[pi] | portInstanceOf[pc] in Sink)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Sink => all pi : portInstances[ps] |
all pc: connection[pi] |portInstanceOf[pc] in Source)
AConstraint4: A receptacle instance should connect to at most one facet instance.
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Receptacle =>
all pi : portInstances[ps] | sole connection[pi] )
AConstraint5: A port instance pi1 can only be connected to a port instance pi2 if pi1 and pi2 have the same port type.
all pi : setPortInstances |
(some connection[pi] => all p: connection[pi] |
(portInstanceOf[pi].ptype = portInstanceOf[p].ptype))
Assertion1: Each ComponentInstance is associated with exactly one ComponentSchema .
assert OneSchemaPerInstance {
all s: State |
all ci: s.setComponentInstances |
one s.componentInstanceOf[ci]
}
check OneSchemaPerInstance for 10
Assertion2: Each port instance pi of a component instance ci have a corresponding port schema ps in the component schema cs associated with ci.
assert AllInstancePortsInSchema {
all s: State |
all ci: s.setComponentInstances |
let cs = s.componentInstanceOf[ci] |
all pi: s.instancePorts[ci] |
s.portInstanceOf[pi] in cs.schemaPorts
}
check AllInstancePortsInSchema for 10
5.3.1 New Component Instance
This operation models a transformation of the system where an new component instance ci (along with all its associated port instances) of component schema cs is allocated. In the post state, the new instance should not be connected to any other component instances. The 'New' operation is more complicated than 'Dispose' because one needs to ensure that port structure of the newly created component instance matches the port structure of the component schema cs.
fun newComponentInstance(s,s': State, ci: ComponentInstance, cs: ComponentSchema ){
//pre condition
not ci in s.setComponentInstances
no s.instancePorts[ci]
all c: ComponentSchema |
not ci in s.componentInstances[c]
//post condition
s'.componentInstances[cs] = s.componentInstances[cs] + ci
s'.setComponentInstances = s.setComponentInstances+ci
#(s'.setPortInstances) = #(s.setPortInstances)+ #(cs.schemaPorts)
all ps: cs.schemaPorts |
one pi: PortInstance |
(not pi in s.portInstances[ps]) &&
(pi in s'.portInstances[ps]) &&
(not pi in s.setPortInstances) &&
(pi in s'.setPortInstances) &&
(pi in s'.instancePorts[ci]) &&
(no s'.connection[pi]) &&
(no s.connection[pi])
//frame condition
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all pi: s.setPortInstances |
(s.instancePartOf[pi] = s'.instancePartOf[pi]) &&
(s.portInstanceOf[pi] = s'.portInstanceOf[pi]) &&
(pi in s'.setPortInstances)
all p: s.setPortInstances |
(some s.connection[p] => s.connection[p] = s'.connection[p]) &&
(no s.connection[p] => no s'.connection[p])
}
run newComponentInstance for 4
5.3.2 Dispose
This operation models a transformation of the system where an existing component instance (along with all its associated port instances) is removed from the system.
fun Dispose(ci: ComponentInstance, s,s':State) {
//pre condition
let cs = s.componentInstanceOf[ci] |
ci in s.componentInstances[cs]
ci in s.setComponentInstances
all pi: s.instancePorts[ci] |
let ps = s.portInstanceOf[pi] |
(pi in s.setPortInstances) && (pi in s.portInstances[ps])
//post condition
all pi1: s.instancePorts[ci] |
all pi2: s.connection[pi1] |
Disconnect(pi1,pi2,s,s')
all pi: s.instancePorts[ci] |
(not pi in s'.setPortInstances) && (no s'.portInstanceOf[pi])
not ci in s'.setComponentInstances
no s'.componentInstanceOf[ci]
s.setComponentInstances = s'.setComponentInstances + ci
#(s.setPortInstances) = #(s'.setPortInstances) +
#((s.componentInstanceOf[ci]).schemaPorts)
//frame condition
all c: s.setComponentInstances - ci |
s.componentInstanceOf[c] = s.componentInstanceOf[c]
all p: s.setPortInstances - s.instancePorts[ci] |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) &&
(s.instancePartOf[p] = s'.instancePartOf[p]) &&
(s.connection[p] = s'.connection[p])
}
run Dispose for 4
5.3.3 Disconnect
This operation models a transformation of the system where an existing connection between port instances pi1 and pi2 is dissolved in the post-state.
fun Disconnect(pi1,pi2: PortInstance, s,s': State) {
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(pi2 in s.connection[pi1]) && (pi1 in s.connection[pi2])
//post condition
(not pi2 in s'.connection[pi1]) && (not pi1 in s'.connection[pi2])
//frame condition
s.setPortInstances = s'.setPortInstances
s.setComponentInstances = s'.setComponentInstances
all ci: s.setComponentInstances |
s.componentInstanceOf[ci] = s'.componentInstanceOf[ci]
all pi: s.setPortInstances |
(s.portInstanceOf[pi] = s'.portInstanceOf[pi]) &&
(s.instancePartOf[pi] = s'.instancePartOf[pi])
all pi: s.setPortInstances - pi1 - pi2 |
s.connection[pi] = s'.connection[pi]
}
run Disconnect for 4
5.3.4 ConnectSourceSink
This operations forms a connection between port instance pi1 (an event source) and port instance pi2 (an event sink). You must write pre-conditions to guarantee (among other things) that pi1 and pi2 are indeed source and sink ports. Again, make sure you include pre- conditions and frame conditions to maintain the constraints that were defined in assignment one.
fun ConnectSourceSink(pi1,pi2: PortInstance, s,s': State){
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(s.portInstanceOf[pi1] in Source &&
s.portInstanceOf[pi2] in Sink) ||
(s.portInstanceOf[pi2] in Source &&
s.portInstanceOf[pi1] in Sink)
(not pi1 in s.connection[pi2]) && (not pi2 in s.connection[pi1])
//post condition
(pi1 in s'.connection[pi2]) && (pi2 in s'.connection[pi1])
//frame condition
s.setComponentInstances = s'.setComponentInstances
s.setPortInstances = s'.setPortInstances
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all p: s.setPortInstances |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) &&
(s.instancePartOf[p] = s'.instancePartOf[p])
all p: s.setPortInstances - pi1 - pi2 |
s.connection[p] = s'.connection[p]
}
run ConnectSourceSink for 4
5.3.5 ConnectFacetReceptacle
This operations forms a connection between port instance pi1 (a Facet) and port instance pi2 (a Receptacle). You must write pre-conditions to guarantee (among other things) that pi1 and pi2 are indeed facet and receptacle ports. Again, make sure you include pre-conditions and frame conditions to maintain the constraints that were defined in assignment one (e.g., recall that a receptacle should be connected to at most one facet).
fun ConnectFacetReceptacle(pi1,pi2: PortInstance, s,s': State){
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(s.portInstanceOf[pi1] in Facet &&
s.portInstanceOf[pi2] in Receptacle) ||
(s.portInstanceOf[pi2] in Facet &&
s.portInstanceOf[pi1] in Receptacle)
(not pi1 in s.connection[pi2]) && (not pi2 in s.connection[pi1])
#(s.connection[pi2])=0 else #(s.connection[pi1])=0
(s.portInstanceOf[pi1] in Facet => #(s.connection[pi2])=0 ) ||
(s.portInstanceOf[pi2] in Facet => #(s.connection[pi1])=0 )
//post condition
(pi1 in s'.connection[pi2]) && (pi2 in s'.connection[pi1])
//frame condition
s.setComponentInstances = s'.setComponentInstances
s.setPortInstances = s'.setPortInstances
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all p: s.setPortInstances |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) &&
(s.instancePartOf[p] = s'.instancePartOf[p])
all p: s.setPortInstances - pi1 - pi2 |
s.connection[p] = s'.connection[p]
}
run ConnectFacetReceptacle for 4
5.3.6 Assertions
4.3.6.1 The state should be the same after dispose and new a component instance.
assert DisposeAndNewComponentInstance {
all s,s': State, ci: ComponentInstance, cs: ComponentSchema |
Dispose(ci,s,s') && newComponentInstance(s,s', ci, cs) =>
s=s'
}
check DisposeAndNewComponentInstance for 9
4.3.6.2 The state should be the same after connect and disconnect facet and receptacle.
assert ConnectAndDisconnectFacetReceptacle {
all s,s': State, pi1, pi2: PortInstance |
ConnectFacetReceptacle(pi1,pi2,s,s') &&
Disconnect(pi1,pi2,s,s') => s=s'
}
check ConnectAndDisconnectFacetReceptacle for 8
4.3.6.3 The state should be the same after connect and disconnect source and sink.
assert ConnectAndDisconnectSourceSink {
all s,s': State, pi1, pi2: PortInstance |
ConnectSourceSink(pi1,pi2,s,s') && Disconnect(pi1,pi2,s,s') =>
s=s'
}
check ConnectAndDisconnectSourceSink for 9
This Software Quality Assurance Plan (SQAP) describes the standards, processes and procedures used to support the delivery of a high-quality and professional project of Component Assembly Description Compiler. The quality assurance process is concerned with establishing the authority of the SQAP function, standards, procedures, policies, and monitoring, and evaluation processes to determine quality in relation to established standards.
(1) IEEE Standard for Software Quality Assurance Plans (IEEE Std 730-1998).
(2) IEEE Guide for Software Quality Assurance Planning (IEEE Std 730.1-1995).
(3) Software Project Management --- A United Framework (Walker Royce, 2001).
Committee: Drs. John Hatcliff, Matthew Dwyer, and William Hankley
Major professor: Dr. John Hatcliff
Developer: Shufeng Li
In phase I, the developer must finish
a) Project overview
b) Cost estimate
c) Project plan
d) Requirement specification
In Phase II, the developer must finish
a) Detailed design (including object model and sequence diagram)
b) SQA plan
c) Test plan
d) Formal technical review
e) Formal specification
In Phase III, the developer must finish
a) Source code
b) Testing
c) Evaluation
d) User manual
The developer is responsible for designing and implementing the project under the supervision of the major professor, Dr. Hatcliff. The developer shall also write all the required documents and report to all the committee members in the form of presentations at the end of each phase.
The major professor suggests the topic of the project and general requirements, supervises and audits the whole development process of the project.
The committee will oversee and review the work performed by the developer, provide feedback and advice, and audit the whole development process during the three presentations of the project.
The purpose is to obtain a good quality product of software. As a minimum, Software Quality Assurance requires the following documents:
1) SW requirements specifications,
2) SW design description,
3) User documentation.
The SQAP activities with each document review must be scheduled in accordance with the development life cycle of the project.
6.4.2.1 SW requirements specification (SRS)
The purpose of the SRS is to provide a description of the critical requirements (functions, performances, design constraints, attributes, etc.) of the software and external interfaces. The SRS should be developed under IEEE Recommended Practice for Software Requirements Specifications (IEEE Std 830-1998) standard. When the CADC SRS is developed, a review which the major advisor shall be involved in is to check its accuracy, consistency, completeness, verifiability, traceability, and so on. If any of these is not right, then the developer should correct it.
6.4.2.2 SW design description (SDD)
The SDD is a technical description of how the software will meet the requirements of SRS. Its most important function is to describe each component of the CADC project after decomposing it into several separate functions.
The SDD should be consisting of the following documents:
1) Object models
2) Sequence diagrams
3) Scenario diagrams
And algorithms shall be written in pseudo code or a chunk of real code.
Since this project is only a component of Cadena system, the user only needs to push some buttons to involve this project. The user documentation only identifies the minimum content and description of the followings: user interaction with the software, input and output specifications, system limitations, anticipated errors and user responses.
The purpose of this section is to identify the standards, practices, conventions, and metrics that will be applied to develop the CADC project. Compliance with these items is achieved by reviews and inspection.
All documents, such as, the software requirements specification (SRS), and software quality assurance plan (SQAP), shall be developed based on IEEE Software Engineering Standards. The format should follow the requirement of MSE portfolio.
Formal specifications will be expressed using Alloy Analyzer.
Java will be used to code CADC project. The comments, identifier names, indentation, and file and package naming conventions of the source code should follow the Java programming standards.
Testing will be carried out in a systematic way. The exact details of testing will be included in the Test Plan (TP).
Milestones are set for each workflow in each phase. The milestones shall be used to manege the process in which the CADC project is developed.
6.5.6.2 Development time and productivity
The staff hours will be logged toward the project, and shall be kept in engineering notebook.
The developer and the major advisor shall be involved for reviewing the major tasks. The minimal required ones shall be the reviews for SRS and SDD. There shall be three formal presentations prepared by the developer and evaluated by the committee at the end of each phase to evaluate the project.
Test needs to test the product for each stage, component, and item by using unit, integration, and system tests. The developer is responsible to test the CADC project. This task is operated based on the test plan.
The tool will be used is Junit-3.8.1, which is available though: http://www.junit.org/index.htm.
On the Unix machines, Concurrent Versions System (CVS) shall be used to store all documents and code (including all deltas) as well as the detailed logs of change intentions.
The standard UNIX file permission standard shall be used to control access to files. The electronical backups shall also be used to store work.
The OpenCCM, OpenORB, and IBM Eclipse manufacturers are identified as our suppliers. We should also ensure that we have the up-to-date software releases, documentations to cover new releases/updates.
JIIC01
The test plan for the Java Implementation of IDL Configuration product should support the objectives described below.
This test plan covers a full unit test and an integration test of the Java Implementation of IDL configuration product. It includes the tests for Java assembly code generation procedures, Cadena XML file generation procedures, and KSU Event Service XML file generation procedures.
This test plan was created based on the following document.
· Java Implementation of IDL configuration Requirement Specification
· JIIC Software design descriptions
· OpenCCM-0.5 document
· OEP Software User Manual
All items that make up the JIIC component will be tested during the software test life cycle.
Type Library
Java Assembly code generation PROGRAM_Lib (JIIC)
Cadena XML configuration file generation PROGRAM_Lib (XMLGEN)
Facet integration configuration file generation PROGRAM_Lib (XMLGEN)
The following scenarios from Boeing Boldstroke OEP are the main scenarios to be tested.
· BasicSP scenario
· ModalSP scenario
· MediumSP scenario
· MultiRateSP scenario
· BasicMP scenario
· MultiRateMP scenario
The following features (specification number followed by description) will be tested for the system test.
The following approaches will be applied on all the components of the JIIC project to carry the coverage test, regression test, functional test, unit test, and integration test.
Assertions are useful constraints that can check the preconditions, post-conditions, and invariants in an efficient and dependable way. Insert assertion statements where those pre or post conditions should hold.
Using coverage test, the developer can derive test cases that all statements have been executed at least once within a module. To do that, some instrument code shall be inserted into all the blocks so that the statement coverage can be calculated by counting which statements are executed.
The outputs of these three project components are files. The regression test could be done in this way: each time some modification is added into the code, comparing the latest output file with the previous versions. If no difference except the new added part found, then it can be claimed that the modification does not violate the previous code. Finding the difference process could be carried out by some UNIX commands or other tools, such as XML diff.
7.6.4.1 BasicSP scenario
A: Task identifier: BSP-1, generating Java assembly code
Expected result: a Java file should satisfy the Java assembly criteria as defined in software requirement specification.
B: Task identifier: BSP-2, generating Boeing OEP XML configuration file
Expected result: a XML file should satisfy the Boeing OEP configuration criteria as defined in OEP Software User Manual.
C: Task identifier: BSP-3, generating KSU Event Service XML configuration file
Expected result: XML file should satisfy the KSU Event Service XML configuration criteria as defined in software requirement specification.
7.6.4.2 MediumSP scenario
A: Task identifier: MESP-1, generating Java assembly code
Expected result: Java file should satisfy the Java assembly criteria as defined in software requirement specification.
B: Task identifier: MESP-2, generating Boeing OEP XML configuration file
Expected result: XML file should satisfy the Boeing OEP configuration criteria as defined in OEP Software User Manual.
C: Task identifier: MESP-3, generating KSU Event Service XML configuration file
Expected result: XML file should satisfy the KSU Event Service XML configuration criteria as defined in software requirement specification.
7.6.4.3 Other scenarios
Other scenarios, such as ModalSP scenario, MultiRateSP scenario, BasicMP scenario, and MultiRateMP scenario, follow the same testing processes as described above.
7.6.4.4 Error messages
For the following cases, the program should yield some meaning error messages for user to read.
a: the property file does not contain some instance information.
b: the input scenario file is empty.
c: the output file is not reachable, or there is no enough space for the output.
a. The Java assembly code should be syntax error free as determined by running code through javac.
b. Manual inspection reveals no errors.
c. Java code should be used in a successful build and execution of the system.
a. The XML file should be syntax error free by display it though Internet Explorer.
b. Manual inspection reveals no errors.
c. XML should be used in a successful build and execution of Boeing OEP system.
a. The XML file should be syntax error free by displaying it though Internet Explorer.
b. Manual inspection reveals no errors.
c. The KSU Event Service configuration XML file shall be used in a successful execution of the KSU event service connection system.
If one of these tests failed, then this round test is failed.
If the scenario file, IDL file, or the CPS file is not available, the test should be suspended.
When a new version of the JIIC component is transmitted to the test procedures after a suspension occurred, a regression test will begin.
The following critical documents should be generated after test completion:
1) Test Plan
2) Test Case specifications
3) Resolution of defects
4) Test Summary Report
|
No. |
Task |
Predecessor tasks |
Effort |
Finish date |
|
1 |
Prepare test plan |
Complete JIIC design description (JIIC-03) |
4 |
01-25-03 |
|
2 |
Prepare test case specification |
Complete corresponding test plans (Task 1) |
4 |
01-31-03 |
|
3 |
Functional test for java generation part |
Task 2 |
3 |
7-01-03 |
|
4 |
Unit test for java generation |
Task 3
|
4 |
7-05-03 |
|
5 |
Execute java assembly code |
Task 4 |
4 |
7-09-03 |
|
6 |
Performance test for java code generation part |
Task 5 |
1 |
7-10-03 |
|
7 |
Functional test for java generation part |
Task 2 |
3 |
7-13-03 |
|
8 |
Unit test for java generation |
Task 7
|
4 |
7-17-03 |
|
9 |
Execute java assembly code |
Task 8 |
4 |
7-21-03 |
|
10 |
Performance test for java code generation part |
Task 9 |
1 |
7-22-03 |
|
11 |
Functional test for java generation part |
Task 2 |
3 |
7-25-03 |
|
12 |
Unit test for java generation |
Task 11
|
4 |
7-29-03 |
|
13 |
Execute java assembly code |
Task 12 |
4 |
8-03-03 |
|
14 |
Performance test for java code generation part |
Task 13 |
1 |
8-04-03 |
JIIC product is coded in Java-language, so it will run on the design platforms. The operating system Linux will be used to execute these tests.
The generated java assembly file will run with OpenCCM-0.5 and OpenORB-1.3.
It will be integrated with IBM Eclipse environment.
Junit testing tool will be used for the whole testing activities.
The developer is responsible for all the testing tasks.
It shall be approved by three committee members.
The JIIC project adopts the visitor design pattern to implement the whole process. In this session, the visitor pattern will be introduced. The following sessions shows the object model, sequence diagram, and states diagram of the project.
The purpose of the Visitor Pattern is to allow you perform operations on elements of a data structure in a uniform way. By doing this, the operation being performed on a structure can be changed without changing the classes of the elements on which it operates.
The key of this structure is creating a visitor for each operation, and letting each object accept the appropriate visitor. Figure 1 illustrates the object model of the visitor design pattern. Figure 7 [13] is the Java code for this model showed in figure 6 [13].
Figure 6 Visitor Design Pattern
abstract class AElement {
public abstract void accept(Visitor v);
}
class ConcreteElementA extends AElement {
public void operationA() {
System.out.println("Doing operation A");
}
public void accept(Visitor visitor) {
visitor.visitConcreteElementA(this);
}
}
abstract class AVisitor {
public abstract void visitConcreteElementA(ConcreteElementA e);
}
class ConcreteVisitor1 extends AVisitor {
public void visitConcreteElementA(ConcreteElementA ceA) {
ceA.operationA();
}
}
public class VisitorClient {
public static void main(String[] args) {
ConcreteVisitor1 visitor = new ConcreteVisitor1();
AElement[] element = new AElement[2];
element[0] = new ConcreteElementA();
element[1] = new ConcreteElementA();
for (int i = 0; i < 2; i++)
element[i].accept(visitor);
}
}
Figure 7 the classes structure for figure 1
The “accept” method in the ConcreteElement classes is the key of this pattern. The Visitor is passed in to the accept method, and that visitor is told to execute its visit method, and is handed the node by the node itself[1]. This method makes the code be robust, because all of the decision made on what to execute where and when it is all taken care of by object dispatching. Nothing ever needs to be checked.
The visit method in every Visitor, including the ConcreteVisitors, performs the operations on the elements of the data structure. The elements of data structure however, only deal with the abstract Visitor, hence only have one method (accept()) that deals with it. The “accept()” method is overridden in each concrete element, which only calls its respective method in the corresponsive concrete visitor.
The major advantage of using this pattern is that it is very easy and simple to add new operations to perform on the existing data structure. All you need to do is create a new Visitor and define the operation there.
There are three reused components in this project. They are defined and tested by other members in our group.
The first one is an interface ASTVisitor. It defines the visit() operations for each object in the abstract syntax tree (AST), whose grammar is defined in document Requirement Specification. Other visitors will use this interface as their template.
The second one is the DefaultVisitor class. It implements the interface ASTVisitor and all the visit() operations. All my client classes implement this class to implement the visit() operations on every node in detail.
The third part is the definitions of all elements in AST. Class Node is just an abstract class which defines an apply(ASTVisitor, Object) method, which is accept() method in figure 6. It takes the ASTVisitor and directs the visitor to the corresponding operations. All other elements, like DataConnection and InstanceDecl, implement this Node class. So the apply operation is inherited automatically. (Here, only several objects are illustrated.)
This structure follows the Visitor design pattern very well except it uses apply() instead of accept() as the name of acceptation operation.
Figure 8: Structure of the reused components
This session presents the object models for the three components of the JIIC project. The following three figures are the object diagrams for each part of the project. They all use the structure illustrated in section 2 as the design base to implement all the tasks. Hence, they are very similar.
Figure 9: object diagram for Glue code generator
Figure 10: Object diagram for KSU Event Service connection XML file generator
Figure 11: Object diagram for OEP XML file generator
Figure 12: Sequence diagram for glue code generator
Figure 13: Sequence diagram for KSU Event Service connection XML file generator
Figure 14: Sequence diagram for OEP XML file generator
Software formal inspections are in-process technical reviews of a product of the software life cycle conducted for the purpose of finding and eliminating defects[15]. It is a formal well defined software quality assurance activity. Formal technical review and inspection can be applied to any product artifact during the early stage of product development, such as requirements, design, and code.
In this document, a formal checklist for implementation phase is provided for inspectors to use. The purpose of the source code inspection is to ensure and verify that the code meets the approved requirements, verify that the code implements the detailed design, and that all required/applicable standards are satisfied, ensure traceability of the code meets the approved requirements and the detailed design.
Hence, in the checklist, the functionality, data usage, control, package and import, computation, maintenance, clarity, and overall of the source code are listed. The inspectors will be two students in our group.
1) Does each class meet the requirement specification?
2) Does each class have a single purpose?
3) Is there some code in the class which should be a function?
4) Does the code meet the detailed design?
5) Is the code consistent with the performance requirements?
1) General
a. Do all variable names have obvious meanings by themselves?
b. Do all the variables named under the naming conventions of the Java Programming Style Guidelines [17]?
2) Common
a. Are there undefined or unused variables?
b. Are all variables initialized in DATA statements, block DATA, or previously defined by assignments or common usage?
c. Are variables used for only one purpose?
d. Are the correct types used?
3) Array
a. Are all arrays dimensioned?
b. Are all arrays used in the bound?
c. Is each array used for only one purpose?
4) Object pointers
a. Are pointers defined and used as pointers?
b. Are pointers typecast correctly?
1) Are “if_else” and “switch” used clearly?
2) Is “while” rather than “do_while” used whenever possible?
3) Do all conditional expressions are simple?
4) Are executable statements in conditionals avoided?
1) Does each file belong to one package?
2) Are there unnecessary import packages?
1) lexical rules for operators
a. Are unary operators adjacent to their operands?
b. Do assignment and condition operators always have spaces around them?
c. Are all Conventional operators surrounded by a space character?
2) evaluation order
a. Are parentheses used properly for precedence?
b. Does the result depend on the evaluation order?
c. Does the code depend on the order of effects? (e.g. i++, ++i)
1) Is each module easy to change?
2) Is each module independent of specific devices where possible?
1) Comments
a. Is each class commented at the beginning?
b. Is each method commented before the code started?
c. Is each parameter and return type commented?
d. Are all pre-conditions and post-conditions commented?
e. Is each public variable commented?
f. Does the comment style follow the Java Programming Style Guidelines?
2) Layout
a. Is the layout of the code such that the logic is apparent?
b. Are loops indented visually separated from the surrounding code?
c. Are all Java keyword, commas, colons are followed by a space character?
3) lexical control structures
a. Is a standard project-wide (or at least consistent) lexical control structure pattern used?
e.g.
while (exp)
{
statements;
}
or
while (exp){
statements;
}
b. Is the conditional put on a separate line?
e.g.
if (exp)
statements;
Does all code follow the Java Programming Style Guidelines?
This project consists of three components. The first one is called Java assembly code generator, the second one is Boeing OEP configuration XML file generator, and the third one is KSU event service connection configuration XML file generator. These three components use the same input, but work separately. The order is not required.
This project belongs to and is part of Cadena product. It can’t be used outside of Cadena.
Since this project is part of Cadena, an integrated environment for building and modeling CCM systems, there is no explicit user commands to execute the project except pushing buttons. By clicking the magic wand in the menu bar, the Java assembly file and KSU Event Service connection configuration XML file can be generated. To generate Boeing OEP XML file, just click the “xml” button as shows below. Figure15 is the interface for user to use. For more detailed information, please see [18].
Figure 15: The user interface of Cadena
If the input scenario is not available for any reason, it will report “scenario is null”. The program will stop immediately.
If the property information is not available, it will report <component_interface_name> “is not found in” <property_file>. And the program will be terminated.
If the required property file is not found, it will report <property_file> “is not found”. And the program will be terminated.
If the output file can’t open, it will throw an Input/Output exception and terminate the program.
IDL3 file is specified in the OMG CORBA Component Model Specifications, chapter 3.
Please here for details.
Scenario files contain declarations of the component instances, the connections between each other, and other information that comprise a system. Please see here for more details.
As mentioned in 3.2, a property file is needed to generate the Boeing OEP XML file.
The property file provides three kinds of information. First, it provides display information for component homes and component instances. Since names for component/instance in scenario files are different than those in the Boeing OEP XML, names in scenario files must be mapped to the Boeing OEP XML names. For example, if a component instance is named "DataSource" in the scenario file, and we want to display it as "DATA_SOURCE" in the Boeing OEP XML file, then the property for "DataSource" in "toDisplayNames.properties" should appear as: DataSource = DATA_SOURCE. [18]
Secondly, the property file provides some implementation information for component instances. In the current CCM translation of OEP scenarios, one component in OEP may correspond to multiple components defined in the IDL3 file because of a different number of ports. We combine the component instance name and component type name from the scenario file as the key, and we set the corresponding component name in OEP as the value. For example, there may be an instance named "GPS" in the scenario file which implements component type "Device". If "GPS" implements component type "BMDevice" in the OEP XML file, then the property for "GPS" should be written as: GPS_Device = BMDevice. [18]
The third use for the property file is to indicate which level of information is being specified. This is done by setting the model property. The model property indicates whether the model is MediumSP, ModalSP, or BasicSP. For example, the entry "model = BasicSP" would indicate the use of the BasicSP model. [18]
The following is a property example file for BasicSP:
model = basicsp
BMClosedED = BM__CLOSED_ED_COMPONENT
BMDevice = BM__DEVICE_COMPONENT
BMDisplay = BM__DISPLAY_COMPONENT
GPS = GPS
AirFrame = AIRFRAME
NavDisplay = NAV_DISPLAY
EventChannel_EventChannel = EventChannel
GPS_BMDevice = BMDevice
AirFrame_BMClosedED = BMClosedED
NavDisplay_BMDisplay = BMDisplay
The Java assembly code is represented in Java language.
This file is in XML format. The DTD is here.
This file is in XML format. The DTD is here.
This document describes how the testing is done on the project based on the test plan. The descriptions of the testing process, failures, and reliability estimates are included.
Fifteen test cases are used in testing process, where all the test cases are the Cadena scenarios or scenarios created based on them. The testing procedures follow the test approach described in test plan. For more detail information about the test cases, please look at the test plan of this project.
The purpose of this step is to make sure all the statements are executed at least once in one module. To do this, an additional command, such as System.out.print() is inserted in each block. Then the number of blocks covered can be determined.
In this module, the total number of blocks is 53. Four test cases are used to cover all the blocks. The following is the test cases used and their block coverage.
| Scenario name | coverage |
| BasicSP.scenario | 51/53 |
| ModalSP.scenario | 52/53 |
| MediumSP.scenario | 36/53 |
| basicCoverage.scenario | 52/53 |
In this module, the total number of blocks is 27. Three test cases are used to cover all the blocks. The following is the test cases used and their block coverage.
| Scenario name | coverage |
| BasicSP.scenario | 14/27 |
| ModalSP_modified.scenario(modified) | 26/27 |
| ModalSP.scenario(with modified common.idl3, modalsp.idl3) | 27/27 |
In this module, the total number of blocks is 109. Six test cases are used to cover most of the blocks. The following is the test cases used and their block coverage.
| Scenario name | Coverage |
| BasicSP.scenario | 64/109 |
| ModalSP.scenario | 73/109 |
| MediumSP_modified.scenario | 77/109 |
| BasicMP.scenario | 76/109 |
| MulriRateMP.scenario | 75/109 |
| MultirateMP_switch.scenario | 78/109 |
Note: The total coverage is 101/109. Those uncovered blocks deal with error messages due to unfound property information. However, all the properties are found during the test. So there are eight blocks are uncovered.
The purpose of this process is to generate the output files and use them in their corresponding environment. By doing this, one can tell whether the outputs are correct easily. If the output files are correct, then the project works correctly.
The following list the input scenarios and their output files. The number in the “()” is the line number of the outputs.
11.2.1.1 Input and output
| Input | Output | Output test result |
| basicsp.scenario | BasicSP.java (127 lines) | Pass |
| modalsp.scenario | ModalSP.java (279 lines) | Pass |
| mediumsp.scenario | MediumSP.java (432 lines) | Pass |
| basicmp.scenario | BasicMP.java (99 lines) | No |
| multirate.scenario | MultirateMP.java (135 lines) | No |
11.2.1.2 Assembly java code
To do the test, the .java file compiles and executes with the component stub, skeleton, and implementation code. From the screen dump generated by the program, one can observe components being allocated and messages being passed between components according to the semantics defined by the component implementation.
In this process, basicsp scenario, modalsp scenario, and mediumsp scenario pass the test. Other scenarios are not eligible for this process because the implementation code is not ready to use, yet.
11.2.2.1 Input and output
| Input | Output | Output test result |
| basicsp.scenario | connection_basicsp.xml (69 lines) | Pass |
| modalsp.scenario | connection_modalsp.xml (179 lines) | Pass |
| mediumsp.scenario | connection_mediumsp.xml (1369 lines) | No |
| basicmp.scenario | connection_basicmp.xml (47 lines) | No |
| multirate.scenario | connection_multiratemp.xml (135 lines) | No |
11.2.2.2 Connection components through KSU Event Service
To do the test, the connection.xml file configures the component connections via the KSU Event Service. From the screen dump generated by the program, one can observe that the component containers decides the event delivery method and push the event to the Event Channel or make an ERM call as per the semantics specified in the connection.xml.
In this process, basicsp scenario and modalsp scenario pass the test. Other scenarios, such as mediumsp, are not eligible to do so because more information is needed to generate the XML file.
11.2.3.1 Input and output
| Input | Output | Output test result |
| basicsp.scenario | boeing_basicsp.xml (117 lines) | Pass |
| modalsp.scenario | boeing_modalsp.xml (382 lines) | Pass |
| mediumsp.scenario | boeing_mediumsp.xml (2406 lines) | No |
| basicmp.scenario | boeing_basicmp.xml (137 lines) | No |
| multirate.scenario | boeing_multiratemp.xml (272 lines) | No |
11.2.3.2 Connection components through KSU Event Service
To do the test, the boeing_scenario.xml file replaces the OEP scenario .xml file, and compiles and executes with other project files. From the screen dump generated by the OEP scenario project, one can observe messages are the same with the ones yielded with the OEP scenario .xml.
In this process, basicsp scenario and modalsp scenario pass the test. But other scenarios we are using are not eligible to do so because they are different than the real Boeing scenarios.
Besides the scenarios used above, there are several other scenarios are used to test this project. The total test cases are 15. So the failure rate for each module is 0/15 = 0.
To estimate the reliability of the project, we need to understand why we choose the 15 test cases.
The structure of these three modules is the same: walking through a tree data structure. And the tree is consisting of a limited number of objects: a list of component library, a list of rates, a list of location names, and a list of component instances. In a component instance, there are only three kinds of connections: DataConnection, BasicEventConnection, and CorrelatedEventConnection. According to this feature, the following test cases are created. Each test case is designed to visit only one kind of object.
onlyInstances.txt ---
visits component instances where there is no any connection exists
DataConnectionScenario.txt visits ---
component instances where is only DataConnection exists
basicEventConnectionScenario.txt ---
component instances where is only BasicEventConnection exists
correlatedConnectionScenario.txt ---
component instances where is only CorrelatedEvent Connection exists
Other objects in the tree structure are very simple. There is no need to test them separately.
After all these objects are tested, we can draw the conclusion that the walking process for each tree node is working correctly. Then we could test more complicated test cases, such as modalsp scenario and mediumsp scenario. In conclusion, the failure rate for the 15 test cases is 0, so is the failure rate for any further testing.
In this document, we will review and evaluate the project to see whether it accomplishes the ideas presented in the initial overview and meets the quality requirement of the product. We will also review the usefulness of the methodologies, the accuracy of the estimations, and the usefulness of the reviews.
The initial idea about this project to take a scenario file and carry out the scenario assembly process, which includes initializing the environment, and instantiating component homes, and creating component instances. All the information is represented in a Java file. Two XML files can also be generated from the scenario file. One XML file is another format to represents the scenario assembly information. It is used when Boeing OEP scenario is executed. Another XML file represents the connection configuration information when the scenario is connected through KSU Event Service instead of OpenCCM.
This project just implements the whole idea and accomplishes the requirement. The benefits of these three outputs are to increase the productivity of programmer, reduce the complexity to implement large distributed systems, and improve software quality.
a) Correctness
This project has been tested with coverage test and integration test. In coverage test, each block has been executed at least once. There are no redundant blocks in the program. In integration test, most of the generated files are compiled and executed in their corresponding environment successfully.
It also has been tested with some possible abnormal conditions without crashing the whole project.
Hence, the correctness of the project is high.
b) Maintainability
This product uses a variant of Visitor design pattern during the implementation stage. One of the advantages of this pattern is good maintainability. Also, this project follows the Java programming styles guidelines and Cadena developer guidelines. It makes the project is easy to understand and modify by other people. Hence, this project is easy to maintain.
c) Integrity
The integration interface is simple. It only requires a limited number of parameters to pass into the project and starts to operate without any further inputs. So its integrity is high.
d) Usability
The user interface of this project is friendly after it is integrated into Cadena. What user needs to do is just clicking some buttons. There are no special skills required to operate the project. The time required to be familiar with this interface is trivial. In conclusion, the usability of this project is good.
The tree structure-walking pattern, motivated by the visitor design pattern, is used to implement this project. It is very useful, easy to use, easy to maintain, and easy to change. By implementing this structure, the developer does not need to understand the tree structure in detail before applying operations on each node. This makes the structure easy to use. Also, the operation being performed on a structure can be changed without changing the classes of the elements on which it operates. This makes the structure easy to maintain and change. Further more, this pattern makes the structure of this project is simple and easy to read. In result, fewer errors may occur.
The estimation of the cost of the project is not quite accurate. This is due to our whole project, Cadena, is still on the research stage. Frequent changes on the input and output are required. The consequence is that this project should be changed accordingly. The result of this made the project is behind the scheduled.
The estimation of the size of the project is accurate. The lines of code were estimated to be 3,000. The final lines of code are about 2,800.
A property file is needed to generate the Boeing OEP XML configuration file. For a small scenario, this is easy. But for a large scenario, this could be error-prone and tiresome for user to write the property file. So if this property could be generated automatically, or the XML file could be generated without the property at all, this generation process would be easier for user to use.
Another issue needs to be improved is that the generated Boeing OEP XML file is not as exact same as the original XML file. This is due to some information is not captured in scenario files at all. In the future, if more information is added into the scenarios, there are some places are needed to change accordingly.
The third issue needs to be improved is that the correlation event connection. Because how the connection should be connected is still undecided, we just hard coded one correlated event connection in modalsp example. Whenever this issue is settled, this part is needed to change.
ConnectionSpecXMLGenerator.java
[1] CORBA & CCM , OMG
[3] OpenORB
[4] CORBA Component Model: Discussion and Use with OpenCCM (Raphaël Marvie, Philippe Merle)
[5] Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems, John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad (submitted for publication -- SAnToS Laboratory Technical Report 2002-02): www.cis.ksu.edu/cadean
[6] Gerald Brose, Andreas Vogel, Keith Duddy, Java Programming with CORBA, Third Edition, ISBN: 0-471-37681-7, 2001
[7] Pressman, Software Engineering, 5th Edition, ISBN: 0-07-365578-3
[8] Royce, Software Project Management: A Unified Framework, ISBN: 0201309580
[9] JUnit: a simple framework to write repeatable tests
[10] CORBA Component Model Tutorial
[11] The Alloy Analyzer, reference manual
[12] CIS 771 Homework, Assignment 1 & Assignment 2
[13] Software Engineering research network: Programming Patterns Overview
[14] Advanced JavaÔ: Internet Applications Third EditionÓ2002 Art Gittleman
[15] The Software Formal Inspection Process Standard, NASA-STD-2202-93
[16] “NASA Software Formal Inspections Guidebook”, NASA, 1993
[17] Java Programming Style Guidelines
[18] Cadena tutorial
[19] Cadena developer guidelines
[20] Jalopy source code formatter: http://jalopy.sourceforge.net/
[21] Checkstyle Java code coding standard
Boeing OEP XML
KSU Event Service connection file
Java Assembly file
| CompilationUnit | ::= | <SYSTEM> <IDENTIFIER> <LBRACE> ( importLibDeclaration )+ ( importCPSDeclaration )* ( <RATES> <INTEGER_LITERAL> ( ","<INTEGER_LITERAL> )* ";" )? (locationsDeclaration )* ( instanceDeclaration )+ <RBRACE> <EOF> |
| importLibDeclaration | ::= | <IMPORTLIB> libName ( "." "*" )? ";" |
| importCPSDeclaration | ::= | <IMPORTCPS> <IDENTIFIER> ";" |
| locationsDeclaration | ::= | <LOCATIONS> locationDecl ( "," locationDecl )* ";" |
| locationDecl | ::= | <IDENTIFIER> |
| instanceDeclaration | ::= | <INSTANCE> <IDENTIFIER> <IMPLEMENTS> libName ( <ON> <IDENTIFIER> )? <LBRACE> ( connectionDeclaration )* <RBRACE> |
| connectionDeclaration | ::= | <CONNECT> name ( correlatedEvent )? <TO> name ( <RUNRATE> <INTEGER_LITERAL> )? ( <SYNCHRONOUSLY> )? ";" |
| name | ::= | <IDENTIFIER> ( "." <IDENTIFIER> )* |
| libName | ::= | <IDENTIFIER> ( "." <IDENTIFIER> )* |
| nameList | ::= | name ( "," name )* |
Note: correlatedEvent does not exist in input file. It only exists in AST.
module CCM
//signatures
--signature of ComponentSchema
sig ComponentSchema {schemaPorts: set PortSchema}
--signature of PortSchema
sig PortSchema {ptype: PortType, schemaPortOf: ComponentSchema}
part sig Facet, Receptacle, Source, Sink extends PortSchema {}
--signature of PortType
sig PortType {}
part sig EventType, InterfaceType extends PortType {}
--signature of ComponentInstance
sig ComponentInstance {}
sig PortInstance {}
sig State {
setComponentInstances : set ComponentInstance,
setPortInstances : set PortInstance,
componentInstanceOf : ComponentInstance -> ?ComponentSchema,
componentInstances : ComponentSchema? -> ComponentInstance,
portInstanceOf : PortInstance -> ?PortSchema,
portInstances : PortSchema? -> PortInstance,
instancePorts : ComponentInstance? -> PortInstance,
instancePartOf: PortInstance -> ?ComponentInstance,
connection : PortInstance -> PortInstance
}{
componentInstances = ~componentInstanceOf
portInstances = ~portInstanceOf
instancePorts = ~instancePartOf
//each component instance in this state has exactly one Component schema
//others don't have Component schema
all ci: setComponentInstances |
one componentInstanceOf[ci]
all ci: ComponentInstance - setComponentInstances |
no componentInstanceOf[ci]
//each port instance in this state has exactly one Component instance which also belongs to this state
//others don't have Component instance
all pi: setPortInstances |
(one instancePartOf[pi]) && (instancePartOf[pi] in setComponentInstances)
all pi: PortInstance - setPortInstances |
no instancePartOf[pi]
//each port instance in this state has exactly one Port Schema
//others don't have Port Schema
all pi: setPortInstances |
one portInstanceOf[pi]
all pi: PortInstance - setPortInstances |
no portInstanceOf[pi]
//those port instances not in this state don't have any connection
all pi: PortInstance - setPortInstances |
no connection[pi]
// Constraint.3
// Each port instance pi of a component instance ci has a
// corresponding port schema ps in the component schema cs associated
// with ci.
all ci : setComponentInstances |
all pi : instancePorts[ci] |
portInstanceOf[pi] in (componentInstanceOf[ci]).schemaPorts
// Constraint.4
// each port schema ps declared in a component schema cs
// must have a corresponding port instance pi in every component
// instance ci of cs.
all ci : setComponentInstances |
all ps : (componentInstanceOf[ci]).schemaPorts |
one pi : portInstances[ps] | instancePartOf[pi] = ci
// Constraint.5
// connection relation should be symmetric
all pi1 : setPortInstances |
all pi2 : connection[pi1] | (pi1 in connection[pi2])
// Additional.1
// connections must be made between different component instances
// i.e., a component instance cannot connect to itself.
// There are other ways to say this (e.g., the intersection of the
// two sets below is empty). However, one should not simply
// require that the two sets be not equal -- that is not strong
// enough.
all pi : setPortInstances |
all p: connection[pi] |
not instancePartOf[pi] = instancePartOf[p]
// Additional.2
// facet instances should connect to a receptacle instances
// (and vice versa)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Facet => all pi : portInstances[ps] |
all pc: connection[pi] |
portInstanceOf[pc] in Receptacle)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Receptacle => all pi : portInstances[ps] |
all pc: connection[pi] |
portInstanceOf[pc] in Facet)
// Additional.3
// source instances should connect to sink instances (and vice versa)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Source => all pi : portInstances[ps] |
all pc: connection[pi] |
portInstanceOf[pc] in Sink)
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Sink => all pi : portInstances[ps] |
all pc: connection[pi] |
portInstanceOf[pc] in Source)
// Additional.4
// a receptacle should connect to at most one facet
all ci: setComponentInstances |
all ps: (componentInstanceOf[ci]).schemaPorts |
(ps in Receptacle => all pi : portInstances[ps] | sole connection[pi] )
// Additional.5
// each connection must only connect to things of the same type
all pi : setPortInstances |
(some connection[pi] => all p: connection[pi] |
(portInstanceOf[pi].ptype = portInstanceOf[p].ptype))
}
fact instanceChecking {
ComponentSchema$schemaPorts = ~PortSchema$schemaPortOf
}
fact typechecking {
// Constraint.1
// facets/receptacles have interface types
all p : Facet + Receptacle | p.ptype in InterfaceType
// Constraint.2
// source/sinks have event types
all p : Source + Sink | p.ptype in EventType
}
assert OneSchemaPerInstance {
all s: State |
all ci: s.setComponentInstances |
one s.componentInstanceOf[ci]
}
check OneSchemaPerInstance for 10
assert AllInstancePortsInSchema {
all s: State |
all ci: s.setComponentInstances |
let cs = s.componentInstanceOf[ci] |
all pi: s.instancePorts[ci] |
s.portInstanceOf[pi] in cs.schemaPorts
}
check AllInstancePortsInSchema for 10
fun newComponentInstance(s,s': State, ci: ComponentInstance, cs: ComponentSchema ){
//pre condition
not ci in s.setComponentInstances
no s.instancePorts[ci]
all c: ComponentSchema |
not ci in s.componentInstances[c]
//post condition
s'.componentInstances[cs] = s.componentInstances[cs] + ci
s'.setComponentInstances = s.setComponentInstances+ci
#(s'.setPortInstances) = #(s.setPortInstances)+ #(cs.schemaPorts)
all ps: cs.schemaPorts |
one pi: PortInstance |
(not pi in s.portInstances[ps]) && (pi in s'.portInstances[ps]) &&
(not pi in s.setPortInstances) && (pi in s'.setPortInstances) &&
(pi in s'.instancePorts[ci]) && (no s'.connection[pi]) && (no s.connection[pi])
//frame condition
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all pi: s.setPortInstances |
(s.instancePartOf[pi] = s'.instancePartOf[pi]) && (s.portInstanceOf[pi] = s'.portInstanceOf[pi])
&& (pi in s'.setPortInstances)
all p: s.setPortInstances |
(some s.connection[p] => s.connection[p] = s'.connection[p]) && (no s.connection[p] => no s'.connection[p])
}
run newComponentInstance for 4
fun Dispose(ci: ComponentInstance, s,s':State) {
//pre condition
let cs = s.componentInstanceOf[ci] | ci in s.componentInstances[cs]
ci in s.setComponentInstances
all pi: s.instancePorts[ci] |
let ps = s.portInstanceOf[pi] |
(pi in s.setPortInstances) && (pi in s.portInstances[ps])
//post condition
all pi1: s.instancePorts[ci] |
all pi2: s.connection[pi1] |
Disconnect(pi1,pi2,s,s')
all pi: s.instancePorts[ci] |
(not pi in s'.setPortInstances) && (no s'.portInstanceOf[pi])
not ci in s'.setComponentInstances
no s'.componentInstanceOf[ci]
s.setComponentInstances = s'.setComponentInstances + ci
#(s.setPortInstances) = #(s'.setPortInstances) + #((s.componentInstanceOf[ci]).schemaPorts)
//frame condition
all c: s.setComponentInstances - ci |
s.componentInstanceOf[c] = s.componentInstanceOf[c]
all p: s.setPortInstances - s.instancePorts[ci] |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) && (s.instancePartOf[p] = s'.instancePartOf[p]) &&
(s.connection[p] = s'.connection[p])
}
run Dispose for 4
fun Disconnect(pi1,pi2: PortInstance, s,s': State) {
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(pi2 in s.connection[pi1]) && (pi1 in s.connection[pi2])
//post condition
(not pi2 in s'.connection[pi1]) && (not pi1 in s'.connection[pi2])
//frame condition
s.setPortInstances = s'.setPortInstances
s.setComponentInstances = s'.setComponentInstances
all ci: s.setComponentInstances |
s.componentInstanceOf[ci] = s'.componentInstanceOf[ci]
all pi: s.setPortInstances |
(s.portInstanceOf[pi] = s'.portInstanceOf[pi]) && (s.instancePartOf[pi] = s'.instancePartOf[pi])
all pi: s.setPortInstances - pi1 - pi2 |
s.connection[pi] = s'.connection[pi]
}
run Disconnect for 4
fun ConnectSourceSink(pi1,pi2: PortInstance, s,s': State){
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(s.portInstanceOf[pi1] in Source && s.portInstanceOf[pi2] in Sink) ||
(s.portInstanceOf[pi2] in Source && s.portInstanceOf[pi1] in Sink)
(not pi1 in s.connection[pi2]) && (not pi2 in s.connection[pi1])
//post condition
(pi1 in s'.connection[pi2]) && (pi2 in s'.connection[pi1])
//frame condition
s.setComponentInstances = s'.setComponentInstances
s.setPortInstances = s'.setPortInstances
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all p: s.setPortInstances |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) && (s.instancePartOf[p] = s'.instancePartOf[p])
all p: s.setPortInstances - pi1 - pi2 |
s.connection[p] = s'.connection[p]
}
run ConnectSourceSink for 4
fun ConnectFacetReceptacle(pi1,pi2: PortInstance, s,s': State){
//pre condition
(pi1 in s.setPortInstances) && (pi2 in s.setPortInstances)
not s.instancePartOf[pi1] = s.instancePartOf[pi2]
(s.portInstanceOf[pi1]).ptype = (s.portInstanceOf[pi2]).ptype
(s.portInstanceOf[pi1] in Facet && s.portInstanceOf[pi2] in Receptacle) ||
(s.portInstanceOf[pi2] in Facet && s.portInstanceOf[pi1] in Receptacle)
(not pi1 in s.connection[pi2]) && (not pi2 in s.connection[pi1])
//if ((s.portInstanceOf[pi1]).ptype in Facet) then #(s.connection[pi2])=0 else #(s.connection[pi1])=0
(s.portInstanceOf[pi1] in Facet => #(s.connection[pi2])=0 ) || (s.portInstanceOf[pi2] in Facet => #(s.connection[pi1])=0 )
//post condition
(pi1 in s'.connection[pi2]) && (pi2 in s'.connection[pi1])
//frame condition
s.setComponentInstances = s'.setComponentInstances
s.setPortInstances = s'.setPortInstances
all c: s.setComponentInstances |
s.componentInstanceOf[c] = s'.componentInstanceOf[c]
all p: s.setPortInstances |
(s.portInstanceOf[p] = s'.portInstanceOf[p]) && (s.instancePartOf[p] = s'.instancePartOf[p])
all p: s.setPortInstances - pi1 - pi2 |
s.connection[p] = s'.connection[p]
}
run ConnectFacetReceptacle for 4
assert DisposeAndNewComponentInstance {
all s,s': State, ci: ComponentInstance, cs: ComponentSchema |
Dispose(ci,s,s') && newComponentInstance(s,s', ci, cs) => s=s'
}
check DisposeAndNewComponentInstance for 9
assert ConnectAndDisconnectFacetReceptacle {
all s,s': State, pi1, pi2: PortInstance |
ConnectFacetReceptacle(pi1,pi2,s,s') && Disconnect(pi1,pi2,s,s') => s=s'
}
check ConnectAndDisconnectFacetReceptacle for 8
assert ConnectAndDisconnectSourceSink {
all s,s': State, pi1, pi2: PortInstance |
ConnectSourceSink(pi1,pi2,s,s') && Disconnect(pi1,pi2,s,s') => s=s'
}
check ConnectAndDisconnectSourceSink for 9