uchar i;
for(i=0;i<6;i++) {
Isp_Write_Read(1,passwordx[i],0x2000+0x0200*i); } }
4、PUBLIC.C #include
void Delay_ms(uint x) {
uint a,b;
for(a=x;a>0;a--) for(b=100;b>0;b--); }
5、lcd1602.c
#include
uchar code Table1602A[]=%uchar code Table1602B[]=\void delay1602(uint x) {
uint a,b;
for(a=x;a>0;a--) for(b=10;b>0;b--); }
void write1602_com(uchar com)//写指令 {
OUT_1602=com; Lcd1602_RS=0; Lcd1602_RW=0; Lcd1602_EN=0; delay1602(10); Lcd1602_EN=1; delay1602(10); Lcd1602_EN=0; }
void write1602_date(uchar date)//写数据
54
{
OUT_1602=date; Lcd1602_RS=1; Lcd1602_RW=0; Lcd1602_EN=0; delay1602(10); Lcd1602_EN=1; delay1602(10); Lcd1602_EN=0; }
void init_1602(void)//初始化{
write1602_com(0x38); delay1602(20);
write1602_com(0x0c); delay1602(20);
write1602_com(0x06); delay1602(20);
write1602_com(0x01); }
55
1VCC100KUIABBLM358HDR121P6.7C10.1UFR5V1-Rg-IN+IN-VSAD623REF540KC20.1UFOUT6R3-DCVCC7CAPACITOR+RgP122134INPUT8C310UF+11K510K10KR2R1VCC100K5.1K100K32P1.3HMQ2AA2AR?34563.3VC7路电测检体人路电器鸣蜂BUZZER855010K0.01UFC6123LM1117-3.3V1VinVout35V0.1UF路电示显晶1602/12864液图路MQ_2电R65.1KR7R85101K路电源电S13.3VGNDCAVccAvccP6.2/A2Dvss64GND63GNDP6.1/A1AvssP6.2P6.0/A062RST/NMI61P6.160P6.0REST5958TCK57TDKTDO/TDITMSTMSP5.7/TBoutH56TCKTDT2INI255XXT2OUTXT2OXT2INTDOUTP5.6/ACLK54P5.6/smclk5352P5.751P5.650P5.549VSSVDDV0RSWRENBB0BB1BB2BB3BB4BB5BB6BB7CS1CS2REST-VOLED+LED-125V34P3.05P3.16P3.27P4.08P4.19P4.210P4.311P4.412P4.513P4.614P4.715P6.216175V18VRFRSTR1VSSRR2RC2RC1RR1VO22C310UF/16VC1104C2104876543330LED9VC10IB11VDD2OUT12132IN1IN+141IN-151OUT16A1
357968104C3GDO2P2.3GDO0P2.4C1GDNP2.530pP1.6P1.7P2.0GDNCSnSO路电振晶XT2OUTR110UFMSP430F149IPM47K块模盘3*4键K1K2K38MHzC2XT2INRW1C150KP1.5/AT0P2.2/CAOUT/TA0P1.6/AT1P2.1/TAINCLKP1.7/ATP2.0/AC2LK17P2.3/CA0/TA118P2.4/CA1/TA219P2.6/ADCI2CLK2021P2.5/Rosc222300P3.0/STE24P2.7/TAP3.1/SIMO025P3.2/SOMIO26P3.3/UCLK027P3.4/UTXD02829303132P6.4K9K10K11K13K14K153.3VP1.5P1.6P1.7P2.0P2.1P2.2P2.3P2.4P2.5P2.6P2.7P3.0P3.1P3.2P3.3P3.4P6.5P2.6P6.6P1.0P1.1P1.2R110KR2IN4148576KR449.9K附录Ⅱ 路电位复RESTICIICITRTRSC1104C?R1909KCVCVRRTHQQCCNIS-09CDDR31KATitle 热释电传感器BK5K6P6.3K730p0.01UFP5.4GND32OUTVCC156 GND+图路NIS-09C电SizeNumberBDate:File:1234Sheet of 19-Jun-2014dbn By:raw.dD图路电舍宿能C:\\Users\\lx\\Desktop\\asd\\智 +LCD-128645VR247KR31MR41MC40.01UFR52M路电口CC1100接P1.412P1.5SIVDDVDDP2.1C50.01UFSCLKP2.213.3VDVcc2P6.3P6.3/A33P6.4P6.4/A44P6.5P6.5/A55P6.6P6.6/A66P6.7P6.7/A7VREF+7VREF+8XINXINXOUT9XOUT/TCLK10VeREF+VeREF+VeREF-11VERF-/VeREF-P1.012P1.0/TACLKP1.113P1.1/TA0P1.214P1.2/TA1P1.315P1.3/TA2P1.416P1.4/SMCLK48P5.4/MCLK47P5.3/UCLK146P5.2/S0MI145P5.1/SIMO144P5.0/STE143P4.7/TBCLK42P4.6/TB641P4.5/TB540P4.4/TB439P4.3/TB338P4.2/TB237P4.1/TB136P4.0/TB035P3.7/URXD134P3.6/UTXD133P3.5/urxd0P5.4P5.3P5.2P5.1P5.0P4.7P4.6P4.5P4.4P4.3P4.2P4.1P4.0P3.7P3.6P3.5C247UFRW210K56
附录Ⅲ
英文原文及翻译
PLC Modeling and Checking Based on Formal Method
ABSTRACT
High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checkingPLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.
1. Introduction
PLC is an automatic control device that can receive information from sensors, computing device or other PLC logic input signal, and output the logic signal processed. The control algorithm can be written using standard language, such as Ladder Diagram (LD), Structured Text (ST) or Instruction List (IL) [1]. The technique of PLC using programmable language to control large scale integrated circuit has been widely used in industry [2]. Because of safety critical software can cause serious damage to life or property, verification of safety critical software has become an indispensable step required to assure software quality. The present verifying method for the PLC is still stuck by simulation and testing. However, they cannot cover all possible cases, especial whether the design model of PLC to meet the demand. Therefore, the model checking technology is introduced into the field of PLC. To givetheoretical analysis of PLC design becomes important. The primary step of
57
PLC model checking is to the establishment of PLC model, such as establish a model from Function Charts [3]. The PLC model focuses on the establishment of the time attributes [4]. It can be modeled by the method of timed automata [5] or time period modeling method [6]. Thus state space of the model will be decreased compared to timed automata. Either way one choose, eventually an abstract model can be given [7]. How to build a good PLC abstract model is the most important issue to the checking. As the manually modeling is easy to introduce many errors, so the establishment of an integrated modeling and testing tool is very important, and this is one of the issues of concern to this paper. PLC control program runs in real-time operating system (multi-task or single-task); this paper is mainly based on multi-task scheduling PLC system. Section 2 of the article has an introduction to the modeling method of PLC system. Section 3 gives the analysis and improvement of this model as we need to reduce the probability of pseudo-errors. Section IV designs a model checking tool PLC-Checker to check the established model, including introduce the way of converting PLC program into SPIN's input language Promela code. Finally, a classical PLC example is applied to check and a critical couter-example is found by the PLC-Checker.
2. PLC Modeling
There are three steps of model checking: modeling, prop-PLC Modeling and Checking Based on Formal Method 1055erty description, and verification. The most important is how to build the system model. In the system, PLC controller is not isolated, but has interaction with its working environment, driver and human [8]. Therefore, these factors should also be modeling. The environment, human, and the PLC controller is independent and concurrent with each other in logic. Also, the model checker SPIN’s input language Promela is focused on describing the concurrent, so starting from this idea, we build these factors into several concurrent processes to fit the checking from SPIN, it will also accurately describe the system. To describe conveniently, they will be called concurrent entities. PLC controller interacts with the concurrent entities through the symbols in image table.
The symbols of PLC system include I (input port), Q (output port), and M (intermediate relay). Figure 1is a diagram of PLC system model. Time interval modeling strategy: using the flag which specific the bit state of concurrent entities to represent the concurrent entities in the state, without regard to the system clock. This
58