THE Z SPECIFICATION DEPENDENCE GRAPH

The lack of existing solutions makes it really hard to understand formal specification languages since the application domain for representations is useful for the purpose of carrying out certain software engineering operations such as slicing and the computation of program metrics.A Z specification dependence graph is presented in this letter. It draws on the strengths of a range of earlier works and adapts them, if necessary, to the Z language.

Design Rationale for a Wide Spectrum Specification Language FGSPEC

FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the corresponding design(operational)specification which describes“how to do”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided which unifies the wide spectrum specification styles from“what”to“how”.

A PSL Ontology-based Shop Floor Dynamical Scheduler Design

Due to the complex,uncertainty and dynamics in the modern manufacturing environment,a flexible and robust shop floor scheduler is essential to achieve the production goals.A design framework of a shop floor dynamical scheduler is presented in this paper.The workflow and function modules of the scheduler are discussed in detail.A multi-step adaptive scheduling strategy and a process specification language,which is an ontology-based representation of process plan,are utilized in the proposed scheduler.The scheduler acquires the dispatching rule from the knowledge base and uses the build-in on-line simulator to evaluate the obtained rule.These technologies enable the scheduler to improve its fine-tune ability and effectively transfer process information into other heterogeneous information systems in a shop floor.The effectiveness of the suggested structure will be demonstrated via its application in the scheduling system of a manufacturing enterprise.

Reusing Test Cases Based on the Function Point

Reusing test cases from existing test case library is quite common in the software testing field. Testing practice tells us that there is a strong relationship between the granularity of a function unit under testing and that of the test case. A function unit with small granularity usually results in the test cases with the same small granularity. Therefore a test case defined as the function point,i. e.,the smallest size function unit,was provided for the first time.Though test cases with smaller granularity usually have better reusability,the cost of accurately reusing and integrating such test cases is also higher. In order to balance the test case reusability and the cost of test case reuse,a novel test case reuse model based on the function point was proposed in this paper. In this model,a reusable test case for specification-based testing was defined and some reuse strategies and three formal reuse methods were given. Finally,the complete automatic software process was realized by a reusing generation tool. The new method has improved reuse accuracy,while greatly enhances the software productivity.

Specification Language NUJSL Based on JSP and Its Supporting System

This paper presents the specification language NUJSL and its supporting system.NUJSL is a modular specification language based on Jackson Program Design Method(JSP).With the module construction,it is convenient to use NUJSL to write larger specifications.The supporting system supports the incremental develop- ment of software specification in NUJSL,and implements the transformation both from specification to software procedural description in Jackson Schematic Logic(pseudo code)and from procedural description to PASCAL program.

Non-Word Repetition Performance in Mandarin-Speaking Preschool Children With and Without Specific Language Impairment(SLI)

Childhood is a critical period for language development, and it is of great importance to discover normal language development and any specific language impairment （SLI） in child language acquisition and then to give them timely diagnosis and treatment. Also it has been previously shown that the non-word repetition task is an efficient assessment tool to screen out those children suspected with SLI. Based on this premise, the present study examined whether the non-word repetition task can be a suitable screening tool to detect language disorders for preschool children in Mandarin Chinese in China. A non-word repetition task was adapted specifically for this purpose. This study examined differences in non-word repetition performance of Mandarin-speaking preschool children screened by a criterion-referenced diagnostic test of specific language impairment （SLI） （the value of Cronbach Alpha at 0.86）. A sample of 282 children were administered the diagnostic test, and a total of 23 SLI suspects were screened out as their language ability measures deviated from the mean by 1.5 SDs. Results indicated that children with SLI made no error with respect to tone in Mandarin, but they showed great difficulty in non-word repetition skills compared to age-matched controls. The findings confirmed that the non-word repetition task is a culturally nonbiased index of language disorders, and that two syllable non-words can be used to identify language disorder.

Towards a Denotational Semantics of Timed RSL Using Duration Calculus

The Timed RAISE Specification Language (Timed RSL) is an extension of RAISE Specification Language by adding time constructors for specifying real-time applications. Duration Calculus (DC) is a real-time interval logic, which can be used to specify and reason about timing and logical constraints on dura- tion properties of Boolean states in a dynamic system. This paper gives a denotational semantics to a subset of Timed RSL expressions, using Duration Calculus extended with super-dense chop modality and notations to capture time point properties of piecewise continuous states of arbitrary types. Using this semantics, the paper presents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requirements.

Formal verification with HiLLS-specified models:A further step in multi-analysis modeling of complex systems

The multi-analysis modeling of a complex system is the act of building a family of models which allows to cover a large spectrum of analysis methods(such as simulation,formal methods,enactment,...)that can be performed to derive various properties of this system.The High-Level Language for Systems Specification(HiLLS)has recently been introduced as a graphical language for discrete event simulation,with potential for other types of analysis,like enactment for rapid system prototyping.HiLLS defines an automata language that also opens the way to formal verification.This paper provides the building blocks for such a feature.That way,a unique model can be used not only to perform both simulation and enactment experiments but also to allow the logical analysis of properties without running any experiment.Therefore,it saves from the effort of building three different analysis-specific models and the need to align them semantically.